Verifying C++ with STL containers via predicate abstraction

ABSTRACT

This paper describes a flexible and easily extensible predicate abstraction-based approach to the verification of STLusage, and observes the advantages of verifying programsin terms of high-level data structures rather than low-level pointer manipulations. We formalize the semantics of theSTL by means of a Hoare-style axiomatization. The verification requires an operational model conservatively approximating the semantics given by the Standard. Our results show advantages (in terms of errors detected and false positives avoided) over previous attempts to analyze STL usage, due to the power of the abstraction engine and model checker

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 2: T. Ball and S. K. Rajamani. Boolean programs: A model and process for software analysis. Technical Report 2000--14, Microsoft Research, February 2000.
• 3: Kevin Bierhoff, Iterator specification with typestates, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181212]
• 4: N. Blanc, A. Groce, and D. Kroening. Verifying C++ with STL containers via predicate abstraction. Technical Report 506, Computer Science Department, ETH Zurich, 2006.
• 5: Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. What's decidable about arrays? In Verification, Model Checking, and Abstract Interpretation, (VMCAI), volume 3855 of Lecture Notes in Computer Science, pages 427--442. Springer, 2006.
• 6: 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]
• 7: 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
• 8: Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004 [doi>10.1023/B:FORM.0000040025.89719.f3]
• 9: E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. SATABS: SAT-based predicate abstraction for ANSI-C. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3440 of Lecture Notes in Computer Science, pages 570--574. Springer, 2005.
• 10: David R. Cok, Specifying java iterators with JML and Esc/Java2, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181210]
• 11: N. Eén and Niklas Sörensson. An extensible SAT-solver. In Theory and Applications of Satisfiability Testing (SAT), pages 502--518, 2003.
• 12: 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
• 13: Douglas Gregor , Sibylle Schupp, STLlint: lifting static checking from languages to libraries, Software—Practice & Experience, v.36 n.3, p.225-254, March 2006 [doi>10.1002/spe.v36:3]
• 14: 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
• 15: C. A. R. Hoare and N. Wirth. An axiomatic definition of the programming language PASCAL. Acta Informatica, 2, 1973.
• 16: ISO/IEC. ISO/IEC 14882:2003 (E). Programming languages - C++, 2003.
• 17: Bart Jacobs , Frank Piessens , Wolfram Schulte, VC generation for functional behavior and non-interference of iterators, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181209]
• 18: Neelakantan R. Krishnaswami, Reasoning about iterators with separation logic, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181213]
• 19: 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
• 20: Madanlal Musuvathi , David Y. W. Park , Andy Chou , Dawson R. Engler , David L. Dill, CMC: a pragmatic approach to model checking real code, Proceedings of the 5th symposium on Operating systems design and implementation

  Due to copyright restrictions we are not able to make the PDFs for this conference available for downloading

  , December 09-11, 2002, Boston, Massachusetts [doi>10.1145/1060289.1060297]
• 21: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 22: Changqing Wang , David R. Musser, Dynamic Verification of C++ Generic Algorithms, IEEE Transactions on Software Engineering, v.23 n.5, p.314-323, May 1997 [doi>10.1109/32.588523]
• 23: Bruce W. Weide, SAVCBS 2006 challenge: specification of iterators, Proceedings of the 2006 conference on Specification and verification of component-based systems, November 10-11, 2006, Portland, Oregon [doi>10.1145/1181195.1181211]

INDEX TERMS

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

General Terms:
Languages, Verification

Keywords:
C++, STL, iterator, model checking, predicate abstraction, verification