Decidability and Synthesis of Abstract Inductive Invariants

Author Francesco Ranzato



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.30.pdf
  • Filesize: 0.58 MB
  • 21 pages

Document Identifiers

Author Details

Francesco Ranzato
  • Dipartimento di Matematica, University of Padova, Italy

Acknowledgements

I thank Patrick Cousot for comments and suggestions on an earlier version of this paper.

Cite AsGet BibTex

Francesco Ranzato. Decidability and Synthesis of Abstract Inductive Invariants. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.30

Abstract

Decidability and synthesis of inductive invariants ranging in a given domain play an important role in software verification. We consider here inductive invariants belonging to an abstract domain A as defined in abstract interpretation, namely, ensuring the existence of the best approximation in A of any system property. In this setting, we study the decidability of the existence of abstract inductive invariants in A of transition systems and their corresponding algorithmic synthesis. Our model relies on some general results which relate the existence of abstract inductive invariants with least fixed points of best correct approximations in A of the transfer functions of transition systems and their completeness properties. This approach allows us to derive decidability and synthesis results for abstract inductive invariants which are applied to the well-known Karr’s numerical abstract domain of affine equalities. Moreover, we show that a recent general algorithm for synthesizing inductive invariants in domains of logical formulae can be systematically derived from our results and generalized to a range of algorithms for computing abstract inductive invariants.

Subject Classification

ACM Subject Classification
  • Theory of computation → Invariants
  • Theory of computation → Abstraction
Keywords
  • Inductive invariant
  • program verification
  • abstract interpretation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Patrick Cousot. Partial completeness of abstract fixpoint checking. In Proceedings of the 4th International Symposium on Abstraction, Reformulation, and Approximation (SARA'02), volume 1864 of Lecture Notes in Computer Science, pages 1-25. Springer-Verlag, 2000. URL: https://doi.org/10.1007/3-540-44914-0_1.
  2. Patrick Cousot. On fixpoint/iteration/variant induction principles for proving total correctness of programs with denotational semantics. In Proc. 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), volume 12042 of LNCS, pages 3-18. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-45260-5_1.
  3. Patrick Cousot and Radhia 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 (POPL'77), pages 238-252. ACM Press, 1977. URL: https://doi.org/10.1145/512950.512973.
  4. Patrick Cousot and Radhia Cousot. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'79), pages 269-282, New York, NY, USA, 1979. ACM. URL: https://doi.org/10.1145/567752.567778.
  5. Patrick Cousot and Radhia Cousot. Induction principles for proving invariance properties of programs. In D. Néel, editor, Tools & Notions for Program Construction: an Advanced Course, pages 75-119. Cambridge University Press, Cambridge, UK, August 1982. Google Scholar
  6. Patrick Cousot and Radhia Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6(1):69-95, 1999. URL: https://doi.org/10.1023/A:1008649901864.
  7. Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'78), pages 84-96. ACM, 1978. URL: https://doi.org/10.1145/512760.512770.
  8. Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. Inductive invariant generation via abductive inference. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, (OOPSLA'13), pages 443-456. ACM, 2013. URL: https://doi.org/10.1145/2509136.2509511.
  9. Yotam M. Y. Feldman, Neil Immerman, Mooly Sagiv, and Sharon Shoham. Complexity and information in invariant inference. Proc. ACM Program. Lang., 4(POPL), 2019. URL: https://doi.org/10.1145/3371073.
  10. Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham. Bounded Quantifier Instantiation for Checking Inductive Invariants. Logical Methods in Computer Science, Volume 15, Issue 3, 2019. URL: https://doi.org/10.23638/LMCS-15(3:18)2019.
  11. Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham, and Mooly Sagiv. Inferring inductive invariants from phase structures. In Proc. 31st International Conference on Computer Aided Verification (CAV'19), volume 11562 of Lecture Notes in Computer Science, pages 405-425. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_23.
  12. Nathanaël Fijalkow, Engel Lefaucheux, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell. On the Monniaux problem in abstract interpretation. In Proc. 26th International Static Analysis Symposium (SAS'19), volume 11822 of Lecture Notes in Computer Science, pages 162-180. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-32304-2_9.
  13. Robert W. Floyd. Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics, 19:19-32, 1967. Google Scholar
  14. Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Complete abstract interpretations made constructive. In Proceedings of the 23rd International Symposium on Mathematical Foundations of Computer Science (MFCS'98), volume 1450 of Lecture Notes in Computer Science, pages 366-377. Springer, 1998. URL: https://doi.org/10.1007/BFb0055786.
  15. Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361-416, 2000. URL: https://doi.org/10.1145/333979.333989.
  16. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. Polynomial invariants for affine programs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS'18), pages 530-539. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209142.
  17. Michael Karr. Affine relationships among variables of a program. Acta Inf., 6:133-151, 1976. Google Scholar
  18. Zachary Kincaid, John Cyphert, Jason Breck, and Thomas Reps. Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang., 2(POPL), 2018. URL: https://doi.org/10.1145/3158142.
  19. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proc. International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-16), Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  20. Zohar Manna, Stephen Nes, and Jean Vuillemin. Inductive methods for proving properties of programs. Commun. ACM, 16(8):491-502, 1973. URL: https://doi.org/10.1145/355609.362336.
  21. Antoine Miné. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages, 4(3-4):120-372, 2017. URL: https://doi.org/10.1561/2500000034.
  22. Antoine Miné, Jason Breck, and Thomas W. Reps. An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. In Proc. 25th European Symposium on Programming (ESOP'16), volume 9632 of Lecture Notes in Computer Science, pages 560-588. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_22.
  23. David Monniaux. On the decidability of the existence of polyhedral invariants in transition systems. arXiv CoRR, abs/1709.04382, 2017. URL: http://arxiv.org/abs/1709.04382.
  24. David Monniaux. On the decidability of the existence of polyhedral invariants in transition systems. Acta Inf., 56(4):385-389, 2019. URL: https://doi.org/10.1007/s00236-018-0324-y.
  25. Christian Müller, Helmut Seidl, and Eugen Zalinescu. Inductive invariants for noninterference in multi-agent workflows. In Proc. 31st IEEE Computer Security Foundations Symposium (CSF'18), pages 247-261. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/CSF.2018.00025.
  26. Markus Müller-Olm and Helmut Seidl. A note on Karr’s algorithm. In Proceedings 31st International Colloquium on Automata, Languages and Programming (ICALP'04), volume 3142 of Lecture Notes in Computer Science, pages 1016-1028. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_85.
  27. Peter Naur. Proof of algorithms by general snapshots. BIT Numerical Mathematics, 6(4):310-316, 1966. URL: https://doi.org/10.1007/BF01966091.
  28. Oded Padon, Neil Immerman, Sharon Shoham, Aleksandr Karbyshev, and Mooly Sagiv. Decidability of inferring inductive invariants. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'16), pages 217-231. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837640.
  29. David Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5, 1969. Google Scholar
  30. David Park. On the semantics of fair parallelism. In Dines Bjøorner, editor, Abstract Software Specifications, pages 504-526. Springer Berlin Heidelberg, 1980. Google Scholar
  31. Sharon Shoham. Undecidability of inferring linear integer invariants. arXiv CoRR, abs/1812.01069, 2018. URL: http://arxiv.org/abs/1812.01069.
  32. A. Thakur, A. Lal, J. Lim, and T. Reps. PostHat and all that: Automating abstract interpretation. Electronic Notes in Theoretical Computer Science, 311:15-32, 2015. Fourth Workshop on Tools for Automatic Program Analysis (TAPAS 2013). URL: https://doi.org/10.1016/j.entcs.2015.02.003.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail