research-article

Public Access

Decidability of inferring inductive invariants

Authors:

Aleksandr Karbyshev,

Mooly SagivAuthors Info & Claims

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 217 - 231

https://doi.org/10.1145/2837614.2837640

Published: 11 January 2016 Publication History

Abstract

Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant for the system. A key ingredient in this approach is coming up with the inductive invariant, which is known as invariant inference. This is a major difficulty, and it is often left for humans or addressed by sound but incomplete abstract interpretation. This paper is motivated by the problem of inductive invariants in shape analysis and in distributed protocols. This paper approaches the general problem of inferring first-order inductive invariants by restricting the language L of candidate invariants. Notice that the problem of invariant inference in a restricted language L differs from the safety problem, since a system may be safe and still not have any inductive invariant in L that proves safety. Clearly, if L is finite (and if testing an inductive invariant is decidable), then inferring invariants in L is decidable. This paper presents some interesting cases when inferring inductive invariants in L is decidable even when L is an infinite language of universal formulas. Decidability is obtained by restricting L and defining a suitable well-quasi-order on the state space. We also present some undecidability results that show that our restrictions are necessary. We further present a framework for systematically constructing infinite languages while keeping the invariant inference problem decidable. We illustrate our approach by showing the decidability of inferring invariants for programs manipulating linked-lists, and for distributed protocols.

References

[1]

P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In Logic in Computer Science, 1993. LICS’93., Proceedings of Eighth Annual IEEE Symposium on, pages 160–170. IEEE, 1993.

[2]

P. A. Abdulla and B. Jonsson. Ensuring completeness of symbolic verification methods for infinite-state systems. Theoretical Computer Science, 256(1):145–167, 2001.

Digital Library

[3]

P. A. Abdulla, K. ˇ Cer¯ans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In Logic in Computer Science, 1996. LICS’96. Proceedings., Eleventh Annual IEEE Symposium on, pages 313–321. IEEE, 1996.

Digital Library

[4]

P. A. Abdulla, K. ˇ Cer¯ans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1):109–127, 2000.

Digital Library

[5]

P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In Tools and Algorithms for the Construction and Analysis of Systems, pages 721–736. Springer, 2007.

Digital Library

[6]

P. A. Abdulla, A. Bouajjani, J. Cederberg, F. Haziza, and A. Rezine. Monotonic abstraction for programs with dynamic memory heaps. In CAV’08, pages 341–354, 2008.

Digital Library

[7]

P. A. Abdulla, J. Cederberg, and T. Vojnar. Monotonic abstraction for programs with multiply-linked structures. Int. J. Found. Comput. Sci., 24(2):187–210, 2013.

[8]

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. Formal Methods in System Design, 38(2):158–192, 2011.

Digital Library

[9]

A. R. Bradley. Sat-based model checking without unrolling. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, pages 70–87, 2011.

Digital Library

[10]

A. Carioni, S. Ghilardi, and S. Ranise. Automated termination in model-checking modulo theories. Int. J. Found. Comput. Sci., 24(2): 211–232, 2013.

[11]

V. T. Chakaravarthy. New results on the computability and complexity of points - to analysis. In Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, pages 115–125, 2003.

Digital Library

[12]

C. Chang and H. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1990.

[13]

ISBN 9780080880075.

[14]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269–282, New York, NY, 1979. ACM Press.

Digital Library

[15]

P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 105–118, 2011.

Digital Library

[16]

L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.

Digital Library

[17]

A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63–92, 2001.

Digital Library

[18]

R. W. Floyd. Assigning meanings to programs. In Proceedings of Symposium on Applied Mathematics, number 32, 1967.

[19]

T. Gawlitza, J. Leroux, J. Reineke, H. Seidl, G. Sutre, and R. Wilhelm. Polynomial precise interval analysis revisited. In Efficient Algorithms, Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday, pages 422–437, 2009.

Digital Library

[20]

T. M. Gawlitza and D. Monniaux. Invariant generation through strategy iteration in succinctly represented control flow graphs. Logical Methods in Computer Science, 8(3), 2012.

[21]

S. Ghilardi and S. Ranise. Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010. URL http://dx.doi. org/10.2168/LMCS-6(4:10)2010.

[22]

R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000.

Digital Library

[23]

R. Giacobazzi, F. Logozzo, and F. Ranzato. Analyzing program analyses. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 261–273, 2015.

Digital Library

[24]

G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, pages 326–336, 1952.

[25]

N. Immerman. Descriptive Complexity. Graduate Texts in Computer Science. Springer, 1999.

[26]

S. Itzhaky, A. Banerjee, N. Immerman, A. Nanevski, and M. Sagiv. Effectively-propositional reasoning about reachability in linked data structures. In CAV, volume 8044 of LNCS, pages 756–772, 2013.

Digital Library

[27]

A. Karbyshev, N. Bjorner, S. Itzhaky, N. Rinetzky, and S. Shoham. Property-directed inference of universal invariants or proving their absence. In CAV, 2015.

[28]

J. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95(2), May 1960.

[29]

K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning, pages 348–370. Springer, 2010.

Digital Library

[30]

J. Leroux. The general vector addition system reachability problem by Presburger inductive invariants. In Logic In Computer Science, 2009. LICS’09. 24th Annual IEEE Symposium on, pages 4–13. IEEE, 2009.

Digital Library

[31]

T. Lev-Ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis to work for verification: A case study. In Proc. of the Int. Symp. on Software Testing and Analysis, 2000.

Digital Library

[32]

R. Mayr. Undecidable problems in unreliable computations. Theoretical Computer Science, 297(1):337–354, 2003.

Digital Library

[33]

A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Snowbird, Utah, USA, June 20-22, 2001, pages 221–231, 2001.

Digital Library

[34]

C. Nash-Williams. On well-quasi-ordering finite trees. In Proc. Of the Cambridge Phil. Soc. 59, 1963.

[35]

V. Perrelle and N. Halbwachs. An analysis of permutations in arrays. In Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings, pages 279–294, 2010.

Digital Library

[36]

S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24(3):217–298, 2002.

Digital Library

[37]

P. Schnoebelen. Lossy counter machines decidability cheat sheet. In Reachability Problems, 4th International Workshop, RP 2010, Brno, Czech Republic, August 28-29, 2010. Proceedings, pages 51–75, 2010.

Digital Library

[38]

P. Schnoebelen. Revisiting Ackermann-hardness for lossy counter machines and reset petri nets. In Mathematical Foundations of Computer Science 2010, 35th International Symposium, MFCS 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, pages 616–628, 2010. URL http://dx.doi.org/10.1007/978-3-642-15155-2_54.

Digital Library

[39]

Z. Su and D. Wagner. A class of polynomially solvable range constraints for interval analysis without widenings. Theor. Comput. Sci., 345(1):122–138, 2005.

Digital Library

[40]

A. V. Thakur, A. Lal, J. Lim, and T. W. Reps. Posthat and all that: Automating abstract interpretation. Electr. Notes Theor. Comput. Sci., 311:15–32, 2015.

Digital Library

Cited By

Feldman YSagiv MShoham SWilcox J(2022)Property-directed reachability as abstract interpretation in the monotone theoryProceedings of the ACM on Programming Languages10.1145/34986766:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498676
Müller CSeidl H(2022)Stratified guarded first-order transition systemsFormal Methods in System Design10.1007/s10703-022-00404-9Online publication date: 22-Nov-2022
https://doi.org/10.1007/s10703-022-00404-9
Müller CSeidl H(2021)Stratified Guarded First-Order Transition SystemsStatic Analysis10.1007/978-3-030-65474-0_6(113-133)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_6
Show More Cited By

Index Terms

Decidability of inferring inductive invariants

Recommendations

Decidability of inferring inductive invariants
POPL '16

Induction is a successful approach for verification of hardware and software systems. A common practice is to model a system using logical formulas, and then use a decision procedure to verify that some logical formula is an inductive safety invariant ...
Learning the boundary of inductive invariants

We study the complexity of invariant inference and its connections to exact concept learning. We define a condition on invariants and their geometry, called the fence condition, which permits applying theoretical results from exact concept learning to ...
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Tools and Algorithms for the Construction and Analysis of Systems
Abstract
We present a PDR/IC3 algorithm for finding inductive invariants with quantifier alternations. We tackle scalability issues that arise due to the large search space of quantified invariants by combining a breadth-first search strategy and a new ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2016

815 pages

ISBN:9781450335492

DOI:10.1145/2837614

General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

ACM SIGPLAN Notices Volume 51, Issue 1
POPL '16
January 2016
815 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2914770
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

POPL '16

Sponsor:

SIGPLAN

POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 20 - 22, 2016

FL, St. Petersburg, USA

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
909
Total Downloads

Downloads (Last 12 months)192
Downloads (Last 6 weeks)46

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Feldman YSagiv MShoham SWilcox J(2022)Property-directed reachability as abstract interpretation in the monotone theoryProceedings of the ACM on Programming Languages10.1145/34986766:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498676
Müller CSeidl H(2022)Stratified guarded first-order transition systemsFormal Methods in System Design10.1007/s10703-022-00404-9Online publication date: 22-Nov-2022
https://doi.org/10.1007/s10703-022-00404-9
Müller CSeidl H(2021)Stratified Guarded First-Order Transition SystemsStatic Analysis10.1007/978-3-030-65474-0_6(113-133)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_6
Mathur UMadhusudan PViswanathan M(2020)What’s Decidable About Program Verification Modulo Axioms?Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_10(158-177)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_10
Seidl HMüller CFinkbeiner B(2020)How to Win First-Order Safety GamesVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-39322-9_20(426-448)Online publication date: 16-Jan-2020
https://dl.acm.org/doi/10.1007/978-3-030-39322-9_20
Calvanese DGhilardi SGianola AMontali MRivkin A(2019)Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary AchievementsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.311.9311(53-58)Online publication date: 31-Dec-2019
https://doi.org/10.4204/EPTCS.311.9
Peuter DSofronie-Stokkermans V(2019)On Invariant Synthesis for Parametric SystemsAutomated Deduction – CADE 2710.1007/978-3-030-29436-6_23(385-405)Online publication date: 27-Aug-2019
https://dl.acm.org/doi/10.1007/978-3-030-29436-6_23
Echenim MPeltier NSellami Y(2019)Ilinva: Using Abduction to Generate Loop InvariantsFrontiers of Combining Systems10.1007/978-3-030-29007-8_5(77-93)Online publication date: 14-Aug-2019
https://doi.org/10.1007/978-3-030-29007-8_5
Feldman YWilcox JShoham SSagiv M(2019)Inferring Inductive Invariants from Phase StructuresComputer Aided Verification10.1007/978-3-030-25543-5_23(405-425)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_23
Muller CSeidl HZalinescu E(2018)Inductive Invariants for Noninterference in Multi-agent Workflows2018 IEEE 31st Computer Security Foundations Symposium (CSF)10.1109/CSF.2018.00025(247-261)Online publication date: Jul-2018
https://doi.org/10.1109/CSF.2018.00025
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten