Oded Padon
Neil Immerman
Aleksandr Karbyshev
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.
- 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.Google Scholar
- P. A. Abdulla and B. Jonsson. Ensuring completeness of symbolic verification methods for infinite-state systems. Theoretical Computer Science, 256(1):145–167, 2001. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Carioni, S. Ghilardi, and S. Ranise. Automated termination in model-checking modulo theories. Int. J. Found. Comput. Sci., 24(2): 211–232, 2013.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- C. Chang and H. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1990.Google Scholar
- ISBN 9780080880075.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1):63–92, 2001. Google ScholarDigital Library
- R. W. Floyd. Assigning meanings to programs. In Proceedings of Symposium on Applied Mathematics, number 32, 1967.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google Scholar
- R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- G. Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, pages 326–336, 1952.Google ScholarCross Ref
- N. Immerman. Descriptive Complexity. Graduate Texts in Computer Science. Springer, 1999.Google Scholar
- 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. Google ScholarDigital Library
- A. Karbyshev, N. Bjorner, S. Itzhaky, N. Rinetzky, and S. Shoham. Property-directed inference of universal invariants or proving their absence. In CAV, 2015.Google Scholar
- J. Kruskal. Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture. Transactions of the American Mathematical Society, 95(2), May 1960.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Mayr. Undecidable problems in unreliable computations. Theoretical Computer Science, 297(1):337–354, 2003. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- C. Nash-Williams. On well-quasi-ordering finite trees. In Proc. Of the Cambridge Phil. Soc. 59, 1963.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Decidability of inferring inductive invariants
Recommendations
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 ...
Decidability of inferring inductive invariants
POPL '16Induction 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 ...
Inferring Invariants with Quantifier Alternations: Taming the Search Space Explosion
Tools and Algorithms for the Construction and Analysis of SystemsAbstractWe 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