Automated verification of shape, size and bag properties via user-defined predicates in separation logic. (English) Zbl 1243.68148
Summary: Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In this paper, we propose an automated verification system for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B70 | Logic in computer science |
Keywords:
automated verification; separation logic; entailment checking; inductive shape predicates with size and bag propertiesSoftware:
CVC; Z; ESC/Java; HIP; Smallfoot; MONA; JML; Isabelle/HOL; SMT-LIB; SIMPLIFY; Spec#; Eiffel; z3References:
| [1] | Barnett, M.; Leino, K. R. M.; Schulte, W.: The spec# programming system: an overview, Lecture notes in computer science 3362, 49-69 (2004) |
| [2] | C. Barrett, A. Stump, C. Tinelli, The SMT-LIB standard: version 2.0, in: International Workshop on Satisfiability Modulo Theories. Informal proceedings, 2010. |
| [3] | Berdine, J.; Calcagno, C.; O’hearn, P. W.: Symbolic execution with separation logic, Lecture notes in computer science 3780, 52-68 (2005) · Zbl 1159.68363 · doi:10.1007/11575467 |
| [4] | Berdine, J.; Calcagno, C.; O’hearn, P. W.: Smallfoot: modular automatic assertion checking with separation logic, Lecture notes in computer science 4111, 115-137 (2006) |
| [5] | Bingham, J.; Rakamaric, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs, Lecture notes in computer science 3855, 207-221 (2006) · Zbl 1176.68113 · doi:10.1007/11609773 |
| [6] | Burstall, R. M.; Darlington, J.: A transformation system for developing recursive programs, Journal of ACM 24, No. 1, 44-67 (1977) · Zbl 0343.68014 · doi:10.1145/321992.321996 |
| [7] | Calcagno, C.; Distefano, D.; O’hearn, P. W.; Yang, H.: Compositional shape analysis by means of bi-abduction, , 289-300 (2009) · Zbl 1315.68085 |
| [8] | Chen, C.; Xi, H.: Combining programming with theorem proving, , 66-77 (2005) · Zbl 1302.68241 |
| [9] | Chin, W. N.; David, C.; Nguyen, H. H.; Qin, S.: Automated verification of shape, size and bag properties, , 307-320 (2007) · Zbl 1132.68477 |
| [10] | Chin, W. N.; Khoo, S. C.: Calculating sized types, , 62-72 (2000) |
| [11] | Chin, W. N.; Khoo, S. C.; Qin, S. C.; Popeea, C.; Nguyen, H. H.: Verifying safety policies with size properties and alias controls, , 186-195 (2005) |
| [12] | Cok, D. R.: Reasoning with specifications containing method calls and model fields, Journal of object technology 4, No. 8, 77-103 (2005) |
| [13] | Cok, D. R.; Kiniry, J. R.: ESC/java2: uniting ESC/Java and JML, Lecture notes in computer science 3362, 108-128 (2004) |
| [14] | De Moura, L. M.; Bjørner, N.: Efficient E-matching for SMT solvers, Lecture notes in computer science 4603, 183-198 (2007) · Zbl 1213.68578 · doi:10.1007/978-3-540-73595-3_13 |
| [15] | D. Detlefs, G. Nelson, J.B. Saxe, Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories Palo Alto, 2003. · Zbl 1323.68462 |
| [16] | Distefano, D.; O’hearn, P. W.; Yang, H.: A local shape analysis based on separation logic, Lecture notes in computer science 3920, 287-302 (2006) · Zbl 1180.68112 · doi:10.1007/11691372 |
| [17] | Elgaard, J.; Klarlund, N.; Møller, A.: MONA 1.x: new techniques for WS1S and WS2S, Lecture notes in computer science 1427, 516-520 (1998) |
| [18] | Flanagan, C.; Leino, K. R. M.; Lillibridge, M.; Nelson, G.; Saxe, J. B.; Stata, R.: Extended static checking for Java, , 234-245 (2002) |
| [19] | Gotsman, A.; Berdine, J.; Cook, B.: Interprocedural shape analysis with separated heap abstractions, Lecture notes in computer science 4134, 240-260 (2006) · Zbl 1225.68072 · doi:10.1007/11823230_16 |
| [20] | Harwood, W.; Cavalcanti, A.; Woodcock, J.: A theory of pointers for the UTP, Lecture notes in computer science 5160, 141-155 (2008) · Zbl 1161.68388 · doi:10.1007/978-3-540-85762-4_10 |
| [21] | Hoare, C. A. R.: An axiomatic basis for computer programming, Communications of the ACM 12, No. 10, 576-580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [22] | Hoare, C. A. R.; He, J.: A trace model for pointers and objects, Lecture notes in computer science 1628, 1-17 (1999) · Zbl 0954.68045 |
| [23] | Hoare, C. A. R.: The verifying compiler: a grand challenge for computing research, Journal of ACM 50, No. 1, 63-69 (2003) · Zbl 1032.68868 |
| [24] | Hughes, J.; Pareto, L.; Sabry, A.: Proving the correctness of reactive systems using sized types, , 410-423 (1996) |
| [25] | Ishtiaq, S.; O’hearn, P. W.: BI as an assertion language for mutable data structures, , 14-26 (2001) · Zbl 1323.68077 |
| [26] | Jia, L.; Walker, D.: ILC: a foundation for automated reasoning about pointer programs, Lecture notes in computer science 3924, 131-145 (2006) · Zbl 1178.03077 · doi:10.1007/11693024 |
| [27] | Jones, C.; O’hearn, P.; Woodcock, J.: Verified software: a grand challenge, IEEE computer 39, No. 4, 93-95 (2006) |
| [28] | Kassios, I. T.: Dynamic frames: support for framing, dependencies and sharing without restrictions, Lecture notes in computer science 4085, 268-283 (2006) |
| [29] | König, D.: Theorie der endlichen und unendlichen graphen, Akademische verlagsgesellschaft (1936) · Zbl 0013.22803 |
| [30] | N. Klarlund, A. Moller, MONA Version 1.4 – User Manual. BRICS Notes Series, January 2001. |
| [31] | Klarlund, N.; Schwartzbach, M. I.: Graph types, , 196-205 (1993) |
| [32] | V. Kuncak, Modular data structure verification, Ph.D. Thesis, Massachusetts Institute of Technology, 2007. |
| [33] | Kuncak, V.; Lam, P.; Zee, K.; Rinard, M.: Modular pluggable analyses for data structure consistency, IEEE transactions on software engineering 32, No. 12, 988-1005 (2006) |
| [34] | Kuncak, V.; Nguyen, H. H.; Rinard, M.: An algorithm for deciding bapa: Boolean algebra with Presburger arithmetic, Lecture notes in computer science 3632, 260-277 (2005) · Zbl 1102.03303 · doi:10.1007/11532231 |
| [35] | Lahiri, S.; Qadeer, S.: Verifying properties of well-founded linked lists, , 115-126 (2006) · Zbl 1369.68143 |
| [36] | P. Lam, The hob system for verifying software design properties, Ph.D. Thesis, Massachusetts Institute of Technology, 2007. |
| [37] | Leavens, G. T.; Baker, A. L.; Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java, SIGSOFT software engineering notes 31, No. 3, 1-38 (2006) |
| [38] | Lee, O.; Yang, H.; Yi, K.: Automatic verification of pointer programs using grammar-based shape analysis, Lecture notes in computer science 3444, 124-140 (2005) · Zbl 1108.68396 · doi:10.1007/b107380 |
| [39] | K.R.M. Leino, Specification and verification of object-oriented software, Lecture Notes, Marktoberdorf International Summer School, 2008. |
| [40] | Meyer, Bertrand: Eiffel: the language, (1992) · Zbl 0779.68013 |
| [41] | Moeller, A.; Schwartzbach, M. I.: The pointer assertion logic engine, , 221-231 (2001) |
| [42] | Necula, G.: Proof-carrying code, , 106-119 (1997) |
| [43] | Nelson, G.; Oppen, D. C.: Simplification by cooperating decision procedures, ACM transactions on programming languages and systems 1, No. 2, 245-257 (1979) · Zbl 0452.68013 · doi:10.1145/357073.357079 |
| [44] | Nguyen, H. H.; David, C.; Qin, S. C.; Chin, W. N.: Automated verification of shape and size properties via separation logic, Lecture notes in computer science 4349, 251-266 (2007) · Zbl 1132.68477 · doi:10.1007/978-3-540-69738-1_18 |
| [45] | Nipkow, T.; Paulson, L. C.; Wenzel, M.: Isabelle/HOL – A proof assistant for higher-order logic, Lecture notes in computer science 2283 (2002) · Zbl 0994.68131 |
| [46] | O’hearn, P. W.; Reynolds, J.; Yang, H.: Local reasoning about programs that alter data structures, Lecture notes in computer science 2142, 1-19 (2001) · Zbl 0999.68045 |
| [47] | Pierce, B.: Types and programming languages, (2002) · Zbl 0995.68018 |
| [48] | Pugh, W.: Skip lists: a probabilistic alternative to balanced trees, Communications of the ACM 33, No. 6, 668-676 (1990) |
| [49] | Pugh, W.: A practical algorithm for exact array dependence analysis, Communications of the ACM 35, No. 8, 102-114 (1992) |
| [50] | Reddy, C. R.; Loveland, D. W.: Presburger arithmetic with bounded quantifier alternation, , 320-325 (1978) · Zbl 1282.68142 |
| [51] | Reynolds, J.: Separation logic: a logic for shared mutable data structures, , 55-74 (2002) |
| [52] | Rugina, R.: Quantitative shape analysis, Lecture notes in computer science 3148, 228-245 (2004) · Zbl 1104.68422 · doi:10.1007/b99688 |
| [53] | Sagiv, S.; Reps, T.; Wilhelm, R.: Parametric shape analysis via 3-valued logic, ACM transactions on programming languages and systems 24, No. 3, 217-298 (2002) |
| [54] | Sims, É-J.: Extending separation logic with fixpoints and postponed substitution, Theoretical computer science 351, No. 2, 258-275 (2006) · Zbl 1086.68032 · doi:10.1016/j.tcs.2005.09.071 |
| [55] | Spivey, J. M.: The Z notation: A reference manual, (1989) · Zbl 0777.68003 |
| [56] | Stump, A.; Barrett, C.; Dill, D.: CVC: a cooperating validity checker, Lecture notes in computer science 2404, 500-504 (2002) · Zbl 1010.68720 |
| [57] | J. Tschannen, Automatic verification of eiffel programs, Master’s Thesis, ETH Zurich, 2009. |
| [58] | Walker, D.; Morrisett, G.: Alias types for recursive data structures, Lecture notes in computer science 2071, 177-206 (2000) · Zbl 0985.68007 |
| [59] | Wies, T.; Kuncak, V.; Lam, P.; Podelski, A.; Rinard, M.: Field constraint analysis, Lecture notes in computer science 3855, 157-173 (2006) · Zbl 1176.68130 |
| [60] | H. Xi, Dependent types in practical programming, Ph.D. Thesis, Carnegie Mellon University, 1998. |
| [61] | Yang, H.; Lee, O.; Berdine, J.; Calcagno, C.; Cook, B.; Distefano, D.; O’hearn, P. W.: Scalable shape analysis for systems code, Lecture notes in computer science 5123, 385-398 (2008) · Zbl 1155.68359 · doi:10.1007/978-3-540-70545-1_36 |
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.
