Abstract
We present a novel approach for the automatic generation of inductive loop invariants over non nested loops manipulating arrays. Unlike most existing approaches, it generates invariants containing disjunctions and quantifiers, which are rich enough for proving functional properties over programs which manipulate arrays. Our approach does not require the user to provide initial assertions or postconditions. It proceeds first, by translating body loops into an intermediate representation of parallel assignments, and second, by recognizing through static analysis code patterns that respect stability properties on accessed locations. We associate with each pattern a formula that we prove to be a so-called local invariant, and we give conditions for local invariants to compose an inductive invariant of the complete loop. We also give conditions over invariants to be locally maximal, and we show that some of our pattern invariants are indeed maximal.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aponte, V., Courtieu, P., Moy, Y., Sango, M.: Maximal and Compositional Pattern-Based Loop Invariants - Definitions and Proofs. Technical Report CEDRIC-12-2555, CEDRIC laboratory, CNAM-Paris, France (2011), http://cedric.cnam.fr/fichiers/art_2555.pdf
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)
Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming language Design and Implementation, PLDI 2007, pp. 300–309. ACM, New York (2007)
Bradley, A., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects of Computing 20, 379–405 (2008), doi:10.1007/s00165-008-0080-9
Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)
Cousot, P., Halbwachs, N.: 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 1978, pp. 84–96. ACM, New York (1978)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451–490 (1991)
Denney, E., Fischer, B.: A generic annotation inference algorithm for the safety certification of automatically generated code. In: Proceedings of the 5th International Conference on Generative Programming and Component Engineering, GPCE 2006, pp. 121–130. ACM, New York (2006)
Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs. Comm. ACM 18(8), 453–457 (1975)
Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer (1990)
Verifier, E.C.: http://www.eschertech.com/products/ecv.php (2012)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 235–246. ACM, New York (2008)
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 339–348. ACM, New York (2008)
Harris, W.R., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Program analysis via satisfiability modulo path programs. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, pp. 71–82. ACM, New York (2010)
Hi-Lite: Simplifying the use of formal methods, http://www.open-do.org/projects/hi-lite/
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580 (1969)
Kovács, L.: Invariant Generation for P-Solvable Loops with Assignments. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds.) CSR 2008. LNCS, vol. 5010, pp. 349–359. Springer, Heidelberg (2008)
Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings of the 2009 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC 2009, IEEE Computer Society, Washington, DC (2009)
Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005)
McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
McMillan, K.L.: Lazy Abstraction with Interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)
Miné, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19, 31–100 (2006)
Nielson, H.R., Nielson, F.: Semantics with Applications: a formal introduction. John Wiley & Sons, Inc., New York (1992)
Ottenstein, K.J., Ballance, R.A., MacCabe, A.B.: The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI 1990, pp. 257–271. ACM, New York (1990)
RTCA. Formal methods supplement to DO-178C and DO-278A. Document RTCA DO-333, RTCA (December 2011)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, pp. 318–329. ACM, New York (2004)
Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying Loop Invariant Generation Using Splitter Predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703–719. Springer, Heidelberg (2011)
SPARK Pro (2012), http://www.adacore.com/home/products/sparkpro/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Aponte, V., Courtieu, P., Moy, Y., Sango, M. (2012). Maximal and Compositional Pattern-Based Loop Invariants. In: Giannakopoulou, D., Méry, D. (eds) FM 2012: Formal Methods. FM 2012. Lecture Notes in Computer Science, vol 7436. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32759-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-32759-9_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32758-2
Online ISBN: 978-3-642-32759-9
eBook Packages: Computer ScienceComputer Science (R0)