Skip to main content
SpringerLink
Log in

Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

Our concern is the modular development of a certified static analyzer in the Coq proof assistant. We focus on the extension of the Verified Polyhedra Library—a certified abstract domain of convex polyhedra—with a linearization procedure to handle polynomial guards. Based on ring rewriting strategies and interval arithmetic, this procedure partitions the variable space to infer precise affine terms which over-approximate polynomials. In order to help formal development, we propose a proof framework, embedded in Coq, that implements a refinement calculus. It is dedicated to the certification of parts of the analyzer—like our linearization procedure—whose correctness does not depend on the implementation of the underlying certified abstract domain. Like standard refinement calculi, it introduces data-refinement diagrams. These diagrams relate “abstract states” computed by the analyzer to “concrete states” of the input program. However, our notions of “specification” and “implementation” are exchanged w.r.t. standard uses: the “specification” (computing on “concrete states”) refines the “implementation” (computing on “abstract states”). Our stepwise refinements of specifications hide several low-level aspects of the computations on abstract domains. In particular, they ignore that the latter may use hints from external untrusted imperative oracles (e.g. a linear programming solver). Moreover, refinement proofs are naturally simplified thanks to computations of weakest preconditions. Using our refinement calculus, we elegantly define our partitioning procedure with a continuation-passing style, thus avoiding an explicit datatype of partitions. This illustrates that our framework is convenient to prove the correctness of such higher-order imperative computations on abstract domains.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14

Similar content being viewed by others

Notes

  1. There are several kinds of oracles in the VPL: those based on Farkas certificate for basic polyhedra computations; the linearization strategy in the linearization procedure; etc. In the Coq code, each of these oracles is declared as a “non-deterministic” function in parameter of the code (through an axiom). Here, “non-determinism” is formalized by requiring the results of such functions to inhabit a may-return monad. Section 4.1 recalls the axioms of may-return monads, initially proposed in [13].

  2. Thus, we do not use our refinement calculus in a decompositional (i.e. “top-down”) approach, that builds an implementation by stepwise derivation from a specification. On the contrary, we use our refinement calculus in a compositional (i.e. “bottom-up”) approach, that builds larger “bricks” from smaller “bricks”.

  3. Typically, C\(\sharp \)minor small-step semantics distinguishes infinite loops depending on whether they invoke system calls or not. But, by definition, an infinite loop cannot have runtime errors. Hence, all infinite loops are equivalent for Verasco analyzer. Even better, the analyzer can safely prune any control-flow branch where they appear, exactly like unreachable code.

  4. Thus, the embedding of VPL in Verasco coerces its imperative operators into pure ones. Logically, this coercion remains to assume that VPL oracles are observationally pure. This is potentially wrong, because of potential bugs in these untrusted oracles [13].

  5. Our toy analyzer does not infer loop invariants but requires them from the user. It does not seem too hard to extend our analyzer with inference of loop invariants since the VPL provides a standard (untrusted) widening operator. But, this feature is quite orthogonal to the certification of the analyzer itself. For example, Laporte [19] shows how to program such an untrusted oracle, in order to produce invariants checked by the certified analyzer.

  6. A postcondition is thus in \({{{\mathcal {P}}}}(D\!\times \!D)\) instead of the original \({{{\mathcal {P}}}}(D)\): this standard generalization avoids introducing “auxiliary variables” to represent the input state.

  7. However, in our algebra, \(\sqsubseteq \) corresponds to “refines”, whereas in standard refinement calculus it dually corresponds to “is refined by”. Actually, our convention follows lattice notations of abstract interpretation.

  8. Formally, the status “no alarm is raised” is given by the boolean of our alarm writer monad.

  9. A Kleene algebra is an idempotent (and thus partially ordered) semiring endowed with a closure operator. It generalizes the operations known from regular expressions: the set of regular expressions over an alphabet is a free Kleene algebra.

  10. In Coq jargon, something is “informative” if it is “not a piece of proof” (thus, it remains at extraction).

References

  1. Back, R.J., von Wright, J.: Refinement Calculus—A Systematic Introduction. Graduate Texts in Computer Science. Springer, Berlin (1999)

    Google Scholar 

  2. Besson, F., Jensen, T.P., Pichardie, D., Turpin, T.: Certified result checking for polyhedral analysis of bytecode programs. In: TGC, pp. 253–267 (2010)

  3. Boulmé, S.: Intuitionistic refinement calculus. In: TLCA, LNCS, vol. 4583. Springer (2007)

  4. Boulmé, S.: What is the foreign function interface of the coq programming language? Talk at the coq workshop (2018). https://coqworkshop2018.inria.fr/files/2018/07/coq2018_talk_boulme.pdf

  5. Boulmé, S., Maréchal, A.: Refinement to certify abstract interpretations, illustrated on linearization for polyhedra. In: ITP, LNCS, vol. 9236. Springer (2015)

  6. Boulmé, S., Maréchal, A.: Toward certification for free! Preprint on HAL (2017). https://hal.archives-ouvertes.fr/hal-01558252

  7. Braibant, T., Pous, D.: Deciding kleene algebras in coq. Log. Methods Comput. Sci. 8(1) (2012)

  8. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. TCS 277(1–2), 47–103 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. ACM (1977)

  10. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL. ACM (1978)

  11. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  12. Farouki, R.T.: The Bernstein polynomial basis: a centennial retrospective. Comput. Aided Geom. Des. 29(6), 379–419 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  13. Fouilhé, A., Boulmé, S.: A certifying frontend for (sub)polyhedral abstract domains. In: VSTTE, LNCS, vol. 8471. Springer (2014)

  14. Fouilhé, A., Monniaux, D., Périn, M.: Efficient generation of correctness certificates for the abstract domain of polyhedra. In: SAS, vol. 7935. Springer (2013)

  15. Grégoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: TPHOL, LNCS, vol. 3604, pp. 98–113. Springer (2005)

  16. Handelman, D.: Representing polynomials by positive linear functions on compact convex polyhedra. Pac. J. Math. 132(1), 35–62 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  17. Jourdan, J.H.: Verasco: a formally verified C static analyzer. Theses, Universite Paris Diderot-Paris VII (2016). https://hal.archives-ouvertes.fr/tel-01327023

  18. Jourdan, J.H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: POPL. ACM (2015)

  19. Laporte, V.: Verified static analyzes for low-level languages. Theses, Université Rennes 1 (2015). https://tel.archives-ouvertes.fr/tel-01285624

  20. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  21. Liang, S., Hudak, P.: Modular denotational semantics for compiler construction. In: ESOP, vol. 1058, pp. 219–234. Springer (1996)

  22. Maréchal, A.: New algorithmics for polyhedral calculus via parametric linear programming. Ph.D. thesis, Université Grenoble Alpes (2017)

  23. Maréchal, A., Fouilhé, A., King, T., Monniaux, D., Périn, M.: Polyhedral approximation of multivariate polynomials using Handelman’s theorem. In: VMCAI, pp. 166–184 (2016)

  24. Maréchal, A., Périn, M.: Three linearization techniques for multivariate polynomials in static analysis using convex polyhedra. Technical report TR-2014-7, Verimag research report (2014)

  25. Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: ESOP’05, LNCS, vol. 3444 (2005)

  26. Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI, LNCS, vol. 3855. Springer (2006)

  27. Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1994)

    Google Scholar 

  28. Moscato, M.M., Muñoz, C.A., Smith, A.P.: Affine arithmetic and applications to real-number proving. In: ITP, LNCS, vol. 9236. Springer (2015)

  29. Reynolds, J.C.: The discoveries of continuations. Lisp Symb. Comput. 6(3–4), 233–247 (1993)

    Article  Google Scholar 

  30. Spiwack, A.: Abstract interpretation as anti-refinement. CoRR abs/1310.4283 (2013). http://arxiv.org/abs/1310.4283

  31. The Coq Development Team: The Coq proof assistant reference manual—version 8.4. INRIA (2012–2014)

  32. Wadler, P.: Monads for functional programming. In: AFP, LNCS, vol. 925. Springer (1995)

Download references

Acknowledgements

We thank Alexis Fouilhé, Michaël Périn, David Monniaux and the other members of the Verasco project for their continuous feedback all along this work.

Author information

Authors and Affiliations

  1. Univ. Grenoble Alpes, CNRS, Grenoble-INP, VERIMAG, 38000, Grenoble, France

    Sylvain Boulmé

  2. Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, LIP6, 75005, Paris, France

    Alexandre Maréchal

Authors
  1. Sylvain Boulmé
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandre Maréchal
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sylvain Boulmé.

Additional information

This work was partially supported by French Agence Nationale de la Recherche under the VERASCO project (INS 2011) and by the European Research Council under the EU’s Seventh Framework Programme (FP/2007–2013)/ERC Grant Agreement No. 306595 “STATOR”

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Boulmé, S., Maréchal, A. Refinement to Certify Abstract Interpretations: Illustrated on Linearization for Polyhedra. J Autom Reasoning 62, 505–530 (2019). https://doi.org/10.1007/s10817-018-9492-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-018-9492-2

Keywords

Search

Navigation