Invariant synthesis for combined theories. (English) Zbl 1132.68333
Cook, Byron (ed.) et al., Verification, model checking, and abstract interpretation. 8th international conference, VMCAI 2007, Nice, France, January 14–16, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-69735-0/pbk). Lecture Notes in Computer Science 4349, 378-394 (2007).
Summary: We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.
For the entire collection see [Zbl 1131.68006].
For the entire collection see [Zbl 1131.68006].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Ball, T.; Rajamani, S. K., The Slam project: Debugging system software via static analysis, Proc. POPL, 1-3 (2002), New York: ACM, New York |
| [2] | Bradley, A. R.; Manna, Z.; Sipma, H. B.; Emerson, E. A.; Namjoshi, K. S., What’s decidable about arrays?, Verification, Model Checking, and Abstract Interpretation, 427-442 (2005), Heidelberg: Springer, Heidelberg · Zbl 1176.68116 · doi:10.1007/11609773_28 |
| [3] | Chang, C. C.; Keisler, H. J., Model Theory (1990), Amsterdam: North-Holland, Amsterdam · Zbl 0697.03022 |
| [4] | Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata Theory and Formal Languages, 134-183 (1975), New York: Springer, New York · Zbl 0318.02051 |
| [5] | Colón, M.; Sankaranarayanan, S.; Sipma, H. B.; Hunt, W. A. Jr.; Somenzi, F., Linear invariant generation using non-linear constraint solving, Computer Aided Verification, 420-432 (2003), Heidelberg: Springer, Heidelberg · Zbl 1278.68164 |
| [6] | Cousot, P.; Cousot, R., Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming, Verification, Model Checking, and Abstract Interpretation (2005), Heidelberg: Springer, Heidelberg · Zbl 1111.68503 |
| [7] | Cousot, P.; Cousot, R.; Bruynooghe, M.; Wirsing, M., Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, Programming Language Implementation and Logic Programming, 269-295 (1992), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-55844-6_142 |
| [8] | Flanagan, C.; Leino, K. R.M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R., Extended static checking for Java, Proc. PLDI, 234-245 (2002), New York: ACM, New York |
| [9] | Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science, pp. 19-32. AMS (1967) · Zbl 0189.50204 |
| [10] | Gulwani, S.; Tiwari, A., Combining abstract interpreters, Proc. PLDI, 376-386 (2006), New York: ACM, New York |
| [11] | Henzinger, T. A.; Jhala, R.; Majumdar, R.; Sutre, G., Lazy abstraction, Proc. POPL, 58-70 (2002), New York: ACM, New York · Zbl 1323.68374 |
| [12] | Holzbaur, C.: OFAI clp(q,r) Manual, Edition 1.3.3. Austrian Research Institute for Artificial Intelligence, Vienna. TR-95-09 (1995) |
| [13] | Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Proc. Deduction and Applications, vol. 05431. IBFI Schloss Dagstuhl (2006) |
| [14] | Kapur, D., Zarba, C.: A reduction approach to decision procedures. Technical Report TR-CS-2005-44, University of New Mexico (2005) |
| [15] | Laboratory, T.I.S.: SICStus Prolog User’s Manual. Swedish Institute of Computer Science, PO Box 1263 SE-164 29 Kista, Sweden. Release 3.8.7 (October 2001) |
| [16] | Manna, Z.; Pnueli, A., Temporal verification of reactive systems: Safety (1995), Heidelberg: Springer, Heidelberg |
| [17] | McCarthy, J., Towards a mathematical science of computation, Proc. IFIP Congress, 21-28 (1962), Amsterdam: North-Holland, Amsterdam |
| [18] | Nelson, G.: Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center (1981) |
| [19] | Sankaranarayanan, S.; Sipma, H. B.; Manna, Z.; Giacobazzi, R., Constraint-based linear-relations analysis, Static Analysis, 53-68 (2004), Heidelberg: Springer, Heidelberg · Zbl 1104.68023 |
| [20] | Sankaranarayanan, S.; Sipma, H. B.; Manna, Z., Non-linear loop invariant generation using Gröbner bases, Proc. POPL, 318-329 (2004), New York: ACM, New York · Zbl 1325.68071 |
| [21] | Sankaranarayanan, S.; Sipma, H. B.; Manna, Z.; Cousot, R., Scalable analysis of linear systems using mathematical programming, Verification, Model Checking, and Abstract Interpretation, 25-41 (2005), Heidelberg: Springer, Heidelberg · Zbl 1111.68514 |
| [22] | Schrijver, A., Theory of Linear and Integer Programming (1986), Chichester: Wiley, Chichester · Zbl 0665.90063 |
| [23] | Sofronie-Stokkermans, V.; Nieuwenhuis, R., Hierarchic reasoning in local theory extensions, Automated Deduction - CADE-20, 219-234 (2005), Heidelberg: Springer, Heidelberg · Zbl 1135.03330 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
