publication . Article . Preprint . Other literature type . Part of book or chapter of book . Conference object . 2017

Synthesizing invariants by solving solvable loops

Virgile Prevosto; Steven de Oliveira; Saddek Bensalem;
Open Access English
  • Published: 15 Sep 2017
  • Publisher: HAL CCSD
  • Country: France
Abstract
When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat.
Subjects
free text keywords: Linear transformations, Mathematical transformations, Optimization, Automatic Generation, Formal program verification, Loop invariants, Open source tools, Polynomial optimization problem, Proof obligations, Automation, [INFO]Computer Science [cs], Computer Science - Logic in Computer Science, [ INFO ] Computer Science [cs], invariant generation, linearization, polynomial mapping, Eigenvalues and eigenvectors, Discrete mathematics, Mathematics, Polynomial, Polynomial optimization, Linear map, Loop invariant, Invariant (mathematics)
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
21 references, page 1 of 2

1. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI C Specification Language, 2008.

2. D. P. Bertsekas. Constrained optimization and Lagrange multiplier methods. Academic press, 2014.

3. D. Cachera, T. Jensen, A. Jobin, and F. Kirchner. Inference of polynomial invariants for imperative programs: A farewell to gröbner bases. Science of Computer Programming, 93, 2014.

4. M. A. Colón, S. Sankaranarayanan, and H. B. Sipma. Linear Invariant Generation Using Non-linear Constraint Solving, pages 420-432. Springer Berlin Heidelberg, Berlin, Heidelberg, 2003. [OpenAIRE]

5. A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. In International Conference on Computer Aided Verification, pages 462-475. Springer, 2005.

6. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238-252. ACM, 1977.

7. S. de Oliveira. Pilat. Available at https://github.com/Stevendeo/Pilat.

8. S. de Oliveira, S. Bensalem, and V. Prevosto. Polynomial invariants by linear algebra. Technical Report 16-0065/SDO, CEA, 2016. available at http://steven-de-oliveira.perso.sfr.fr/content/publis/ pilat_tech_report.pdf.

9. L. Gonnord and P. Schrammel. Abstract acceleration in linear relation analysis. Science of Computer Programming, 93:125-153, 2014.

10. B. Jeannet, P. Schrammel, and S. Sankaranarayanan. Abstract acceleration of general linear loops. ACM SIGPLAN Notices, 49(1):529-540, 2014. [OpenAIRE]

11. M. Karr. Affine relationships among variables of a program. Acta Informatica, 6(2):133-151, 1976. [OpenAIRE]

12. F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C: A software analysis perspective. Formal Aspects of Computing, 27(3), 2015.

13. L. Kovács. Aligator: A mathematica package for invariant generation (system description). In Automated Reasoning. Springer, 2008.

14. L. Kovács. Reasoning algebraically about P-solvable loops. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 249-264. Springer, 2008.

15. L. Kovács. A complete invariant generation approach for P-solvable loops. In Perspectives of Systems Informatics. Springer, 2010.

21 references, page 1 of 2
Abstract
When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented in the open-source tool Pilat.
Subjects
free text keywords: Linear transformations, Mathematical transformations, Optimization, Automatic Generation, Formal program verification, Loop invariants, Open source tools, Polynomial optimization problem, Proof obligations, Automation, [INFO]Computer Science [cs], Computer Science - Logic in Computer Science, [ INFO ] Computer Science [cs], invariant generation, linearization, polynomial mapping, Eigenvalues and eigenvectors, Discrete mathematics, Mathematics, Polynomial, Polynomial optimization, Linear map, Loop invariant, Invariant (mathematics)
Funded by
EC| VESSEDIA
Project
VESSEDIA
VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS
  • Funder: European Commission (EC)
  • Project Code: 731453
  • Funding stream: H2020 | RIA
21 references, page 1 of 2

1. P. Baudin, J.-C. Filliâtre, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI C Specification Language, 2008.

2. D. P. Bertsekas. Constrained optimization and Lagrange multiplier methods. Academic press, 2014.

3. D. Cachera, T. Jensen, A. Jobin, and F. Kirchner. Inference of polynomial invariants for imperative programs: A farewell to gröbner bases. Science of Computer Programming, 93, 2014.

4. M. A. Colón, S. Sankaranarayanan, and H. B. Sipma. Linear Invariant Generation Using Non-linear Constraint Solving, pages 420-432. Springer Berlin Heidelberg, Berlin, Heidelberg, 2003. [OpenAIRE]

5. A. Costan, S. Gaubert, E. Goubault, M. Martel, and S. Putot. A policy iteration algorithm for computing fixed points in static analysis of programs. In International Conference on Computer Aided Verification, pages 462-475. Springer, 2005.

6. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238-252. ACM, 1977.

7. S. de Oliveira. Pilat. Available at https://github.com/Stevendeo/Pilat.

8. S. de Oliveira, S. Bensalem, and V. Prevosto. Polynomial invariants by linear algebra. Technical Report 16-0065/SDO, CEA, 2016. available at http://steven-de-oliveira.perso.sfr.fr/content/publis/ pilat_tech_report.pdf.

9. L. Gonnord and P. Schrammel. Abstract acceleration in linear relation analysis. Science of Computer Programming, 93:125-153, 2014.

10. B. Jeannet, P. Schrammel, and S. Sankaranarayanan. Abstract acceleration of general linear loops. ACM SIGPLAN Notices, 49(1):529-540, 2014. [OpenAIRE]

11. M. Karr. Affine relationships among variables of a program. Acta Informatica, 6(2):133-151, 1976. [OpenAIRE]

12. F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C: A software analysis perspective. Formal Aspects of Computing, 27(3), 2015.

13. L. Kovács. Aligator: A mathematica package for invariant generation (system description). In Automated Reasoning. Springer, 2008.

14. L. Kovács. Reasoning algebraically about P-solvable loops. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 249-264. Springer, 2008.

15. L. Kovács. A complete invariant generation approach for P-solvable loops. In Perspectives of Systems Informatics. Springer, 2010.

21 references, page 1 of 2
Any information missing or wrong?Report an Issue