Combining Zonotope Abstraction and Constraint Programming for Synthesizing Inductive Invariants
| Autor: | Eric Goubault, Bibek Kabi, Antoine Miné, Sylvie Putot |
|---|---|
| Přispěvatelé: | Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Algorithmes, Programmes et Résolution (APR), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
0209 industrial biotechnology
Intersection (set theory) Computer science [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 02 engineering and technology Abstract interpretation Domain (software engineering) Polyhedron 020901 industrial engineering & automation Iterative refinement 0202 electrical engineering electronic engineering information engineering Constraint programming 020201 artificial intelligence & image processing [INFO]Computer Science [cs] Invariant (mathematics) Algorithm Abstraction (linguistics) |
| Zdroj: | Software Verification 12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles Software Verification12th International Conference, VSTTE 2020, and 13th International Workshop, NSV 2020, Los Angeles, CA, USA, July 20–21, 2020, Revised Selected Papers 13th International Workshop on Numerical Software Verification (NSV'20) 13th International Workshop on Numerical Software Verification (NSV'20), Jul 2020, Los Angeles, CA, United States. pp.221-238, ⟨10.1007/978-3-030-63618-0⟩ Lecture Notes in Computer Science ISBN: 9783030636173 |
| Popis: | International audience; We propose to extend an existing framework combining abstract interpretation and continuous constraint programming for numerical invariant synthesis, by using more expressive underlying abstract domains, such as zonotopes. The original method, which relies on iterative refinement, splitting and tightening a collection of abstract elements until reaching an inductive set, was initially presented in combination with simple underlying abstract elements: boxes and octagons. The novelty of our work is to use zonotopes, a sub-polyhedric domain that shows a good compromise between cost and precision. As zonotopes are not closed under intersection, we had to extend the existing framework, in addition to designing new operations on zonotopes, such as a novel splitting algorithm based on paving zonotopes by sub-zonotopes and parallelotopes. We implemented this method on top of the APRON library, and tested it on programs with non-linear loops that present complex, possibly non-convex, invariants. We present some results demonstrating both the interest of this splitting-based algorithm to synthesize invariants on such programs, and the good compromise presented by its use in combination with zonotopes with respect to its use with both simpler domains such as boxes and octagons, and more expressive domains such as polyhedra. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|