Advertisement

Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra

  • Alexis Fouilhe
  • David Monniaux
  • Michaël Périn
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

Polyhedra form an established abstract domain for inferring runtime properties of programs using abstract interpretation. Computations on them need to be certified for the whole static analysis results to be trusted. In this work, we look at how far we can get down the road of a posteriori verification to lower the overhead of certification of the abstract domain of polyhedra. We demonstrate methods for making the cost of inclusion certificate generation negligible. From a performance point of view, our single-representation, constraints-based implementation compares with state-of-the-art implementations.

Keywords

Convex Hull Simplex Algorithm Implicit Equality Abstract Domain Redundant Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)Google Scholar
  2. 2.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages (POPL), pp. 84–97. ACM (1978)Google Scholar
  3. 3.
    Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72(1-2), 3–21 (2008)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Jeannet, B., Miné, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), pp. 196–207. ACM (2003)Google Scholar
  6. 6.
    Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)CrossRefGoogle Scholar
  7. 7.
    The Coq Development Team: The Coq proof assistant reference manual. INRIA. 8.4. edn. (2012)Google Scholar
  8. 8.
    Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Technical Report RR-6333, INRIA (2007)Google Scholar
  9. 9.
    Simon, A., King, A.: Exploiting sparsity in polyhedral analysis. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 336–351. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Dutertre, B., De Moura, L.: Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International, computer science laboratory (2006)Google Scholar
  11. 11.
    Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. In: Jeannet, B. (ed.) Tools for Automatic Program Analysis (TAPAS) (2012)Google Scholar
  12. 12.
    Monniaux, D.: A minimalistic look at widening operators. Higher Order and Symbolic Computation 22(2), 145–154 (2009)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Dantzig, G., Thapa, M.N.D.: Linear Programming. Springer (2003)Google Scholar
  14. 14.
    Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 25–44. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Benoy, F., King, A., Mesnard, F.: Computing convex hulls with a linear solver. Theory and Practice of Logic Programming 5(1-2), 259–271 (2005)zbMATHCrossRefGoogle Scholar
  16. 16.
    Monniaux, D.: Quantifier elimination by lazy model enumeration. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 585–599. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  17. 17.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Science of Computer Programming 58(1-2), 28–56 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  18. 18.
    Miné, A., Leroy, X.: ZArith, http://forge.ocamlcore.org/projects/zarith
  19. 19.
    Free Software Foundation: The GNU Multiple Precision Arithmetic Library. 5.0 edn. (2012)Google Scholar
  20. 20.
    Barbosa, C., de Oliveira, D., Monniaux, D.: Experiments on the feasibility of using a floating-point simplex in an SMT solver. In: Workshop on Practical Aspects of Automated Reasoning (PAAR), CEUR Workshop Proceedings (2012)Google Scholar
  21. 21.
    Monniaux, D.: On using floating-point computations to help an exact linear arithmetic decision procedure. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 570–583. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Bugseng: The Parma Polyhedra Library. 1.0 edn. (2012)Google Scholar
  23. 23.
    Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2006)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Alexis Fouilhe
    • 1
  • David Monniaux
    • 1
  • Michaël Périn
    • 1
  1. 1.Verimag – CentreGièresFrance

Personalised recommendations