APRON

Numerical Program Analysis

This projects belongs to the ACI "Sécurité & Informatique"



Home

Partners

The proposal (.ps)

Intermediary report (.pdf, in French)

APRON Interface and librairies

Publications

Widening Benchmarks


Meetings

Paris, 11/08/06

Paris, 09/02/06

Paris, 20/09/05

Palaiseau, 28/06/05

Paris, 15/03/05

Paris, 01/02/05

Paris, 21/01/05

Paris, 17/01/05

Paris, 16/12/04

Toulouse, 15-17/10/04

Paris, 28/10/04


Events

Paris, 21/01/05

London, 07-09/09/05





























Publications
(in no particular order)




  • Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. Patrick Cousot, In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17-19, 2005.

  • The Arithmetic-Geometric Progression Abstract Domain. Jérôme Féret, In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17-19, 2005.

  • David Merchat, Réduction du nombre de variables en analyse de relations linéaires, Thèse de l'Université Joseph Fourier, Grenoble, France, May 18, 2005.

  • B. Jeannet and D. Gopan and T. Reps and M. Sagiv, A Relational Abstraction for Functions, Static Analysis Symposium, SAS'05, London, UK, Sept. 2005.



  • Some ways to reduce the space dimension in polyhedra computations. N. Halbwachs, D. Merchat and L. Gonnord. To appear in Formal Methods in System Design. 2006.

  • Robust and Generic Abstract Domain for Static Program Analysis: the Polyhedral Case, Duong Nguyen Que, thèse de l'École des Mines de Paris, 2006 (à soutenir).

  • GRAPHITE : Polyhedral Analyses and Optimizations for GCC, Sebastian Pop and Georges-André Silber and Albert Cohen and Cédric Bastoul and Sylvain Girbal and Nicolas Vasilache, GNU Compilers Collection Developers Summit 2006, Ottawa, Canada, 28-30 June 2006.

  • Benchmarking Polyhedral Algorithms: Satisfiability and Dual Conversion, Duong Nguyen Que and François Irigoin, Numerical and Symbolic Abstract Domains (NSAD'05), Paris, 21 January 2005.

  • Detecting Affine Loop Invariants using a Modular Static Analysis, François Irigoin, CRI Tech. Report A/368, 2005

  • Static analysis by abstract interpretation of the quasi-synchronous composition of synchronous programs. J. Bertrane, Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, pp. 97-112, Springer-Verlag, 2005

  • Static Analysis of Time-Bounded reactive properties of boolean Symbols, G. Capron, Proceedings of the 21st ACM Symposium on Applied Computing (SAC 2006), Dijon, France, April 23-27, 2006

  • Parametric Abstract Domains, P. Cousot, International workshop on Numerical \& Symbolic Abstract Domains (NSAD 2005)

  • Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming, P. Cousot, Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, pp. 1-24, Springer-Verlag, 2005

  • Numerical Abstract Domains for Digital Filters, Jérôme Feret, International workshop on Numerical \& Symbolic Abstract Domains (NSAD 2005)

  • Combining Widening and Acceleration in Linear Relation Analysis, L. Gonnord and N. Halbwachs, 13th International Static Analysis Symposium, SAS'06, Seoul, Korea, Aug. 2006

  • Loop Invariants on Demand, R. Leino and F. Logozzo, Proceedings of the the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), Tsukuba, Japan, November 3-5, LNCS 3780, Springer-verlag, 2005

  • Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes, F. Logozzo, Submitted for publication.

  • Trace Partitioning in Abstract Interpretation Based Static Analyzers, L. Mauborgne and X. Rival, European Symposium On Programming (ESOP'05), Edimburgh (UK), LNCS 3444, pp. 5-20, Springer-Verlag, 2005

  • Symbolic Methods to Enhance the Precision of Numerical Abstract Domains, A. Miné, Verification, Abstract Interpretation and Model Checking (VMCAI), LNCS 3855, pp. 348-363, Springer-Verlag, 2006

  • Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics, A. Miné, Languages, Compilers, and Tools for Embedded Systems 2006 (LCTES), to be published.

  • The Octagon Abstract Domain, A. Miné, Higher-Order and Symbolic Computation, 2006, to be published.

  • The Trace Partitioning Abstract Domain, X. Rival and L. Mauborgne, TOPLAS, submitted.

  • Extending Separation Logic with Fixpoints and Postponed Substitution, E-J. Sims, Theoretical Computer Science, v. 351, n. 2, pp. 258-275, 2006.

  • An abstract domain for separation logic formulae, E-J. Sims, Proceedings of the 1st International Workshop on Emerging Applications of Abstract Interpretation (EAAI06), Vienna, Austria, 2006.



  • Some ways to reduce the space dimension in polyhedra computations, N. Halbwachs and D. Merchat and L. Gonnord, Formal Methods in System Design, v. 29, n. 1, pp. 78-95, July 2006.

  • Combining Widening and Acceleration in Linear Relation Analysis, L. Gonnord and N. Halbwachs, 13th International Static Analysis Symposium, SAS'06, Ed. Kwangkeun Yi, LNCS 4134, Springer Verlag

  • An abstract domain extending Difference-Bound Matrices with disequality constraints, M. Péron and N. Halbwachs, 8th International Conference on Verification, Model-checking, and Abstract Intepretation, VMCAI'07, Eds. B. Cook and A. Podelski, Nice, France, Jan. 2007.

Valid HTML 4.0! Valid CSS!