Interpolation for data structures

ABSTRACT

Interpolation based automatic abstraction is a powerful and robust technique for the automated analysis of hardware and software systems. Its use has however been limited to control-dominated applications because of a lack of algorithms for computing interpolants for data structures used in software programs. We present efficient procedures to construct interpolants for the theories of arrays, sets, and multisets using the reduction approach for obtaining decision procedures for complex data structures. The approach taken is that of reducing the theories of such data structures to the theories of equality and linear arithmetic for which efficient interpolating decision procedures exist. This enables interpolation based techniques to be applied to proving properties of programs that manipulate these data structures.

REFERENCES

• 1: W. Ackermann. Solvable Cases of the Decision Problem. North-Holland, 1954.
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004 [doi>10.1109/TSE.2004.22]
• 4: David G. Clarke , James Noble , John Potter, Simple Ownership Types for Object Containment, Proceedings of the 15th European Conference on Object-Oriented Programming, p.53-76, June 18-22, 2001
• 5: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 6: W. Craig. Linear reasoning: A new form of the Herbrand-Gentzen theorem. J. Symbolic Logic, 22(3):250--268, 1957.
• 7: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 8: P.J. Downey. Undeciability of Presburger arithmetic with a single monadic predicate letter. Technical Report 18-72, Havard University, 1972.
• 9: Melvin Fitting, First-order logic and automated theorem proving (2nd ed.), Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 10: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 12: Y. Gurevich. The decision problem for standard classes. J. Symbolic Logic, 41(2), 1976.
• 13: John Vogel Guttag, The specification and application to programming of abstract data types., 1975
• 14: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Kenneth L. McMillan, Abstractions from proofs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 14-16, 2004, Venice, Italy
• 15: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 16: C.A.R. Hoare. Proof of correctness of data representations. Acta Inf., 1:271--281, 1972.
• 17: R. Jhala and K.L. McMillan. Interpolant-based transition relation approximation. In CAV 05, LNCS 3576, pages 39--51. Springer, 2005.
• 18: R. Jhala and K.L. McMillan. A practical and complete approach to predicate abstraction. In TACAS 06. Springer, 2006.
• 19: D. Kapur and H. Zhang. An overview of rewrite rule laboratory (RRL). J. Computer and Mathematics with applications, 14(2):91--114, 1995.
• 20: Deepak Kapur and Calogero G. Zarba. A reduction approach to decision procedures. 2005.
• 21: V. Kuncak and M. Rinard. The first-order theory of sets with cardinality constraints is decidable. Technical Report CSAIL 958, MIT, 2004.
• 22: P. Lam, V. Kuncak, and M.C. Rinard. Hob: A tool for verifying data structure consistency. In CC 05, pages 237--241, 2005.
• 23: Barbara Liskov , Stephen Zilles, Programming with abstract data types, Proceedings of the ACM SIGPLAN symposium on Very high level languages, p.50-59, March 28-29, 1974, Santa Monica, California, United States
• 24: A. Mal'cev. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Zh., 3:729--743, 1962.
• 25: K.L. McMillan. Interpolation and SAT-based model checking In CAV 03, LNCS 2725, pages 1--13. Springer, 2003.
• 26: K. L. McMillan, An interpolating theorem prover, Theoretical Computer Science, v.345 n.1, p.101-121, 21 November 2005 [doi>10.1016/j.tcs.2005.07.003]
• 27: S. McPeak and G.C. Necula. Data structure specifications via local equality axioms. In CAV 05, LNCS 3576, pages 476--490. Springer, 2005.
• 28: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 29: Derek C. Oppen, Reasoning About Recursively Defined Data Structures, Journal of the ACM (JACM), v.27 n.3, p.403-411, July 1980 [doi>10.1145/322203.322204]
• 30: Matthew Parkinson , Gavin Bierman, Separation logic and abstraction, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.247-258, January 12-14, 2005, Long Beach, California, USA
• 31: David L. Parnas, The secret history of information hiding, Software pioneers: contributions to software engineering, Springer-Verlag New York, Inc., New York, NY, 2002
• 32: M. Presburger. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt. In Comptes Rendus du Premier Congrès des Mathématicienes des Pays Slaves, pages 92--101, 1929.
• 33: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 34: Aaron Stump , Clark W. Barrett , David L. Dill , Jeremy Levitt, A Decision Procedure for an Extensional Theory of Arrays, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.29, June 16-19, 2001
• 35: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 36: G. Takeuti. Proof Theory. North-Holland, 1987.
• 37: A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 1951.
• 38: A. M. Turing. On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Society, 42:230--265, 1936.
• 39: Volker Weispfenning, The complexity of linear problems in fields, Journal of Symbolic Computation, v.5 n.1-2, p.3-27, February/April 1988 [doi>10.1016/S0747-7171(88)80003-8]
• 40: Calogero G. Zarba, Combining Multisets with Integers, Proceedings of the 18th International Conference on Automated Deduction, p.363-376, July 27-30, 2002
• 41: C.G. Zarba. A quantifier elimination algorithm for a fragment of set theory involving the cardinality operator. In International Workshop on Unification, 2004.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Reliability, Verification

Keywords:
CEGAR, data structure verification, interpolation