Invited talk: the blast query language for software verification

ABSTRACT

blast is an automatic verification tool for checking temporal safety properties of C~programs. blast is based on lazy predicate abstraction driven by interpolation-based predicate discovery. The blast specification language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications.

REFERENCES

• 1: 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
• 2: T. Ball and S.K. Rajamani. SLIC: A specification language for interface checking (of C). Technical Report MSR-TR-2001-21, Microsoft Research, 2002.
• 3: Dirk Beyer , Andreas Noack , Claus Lewerentz, Simple and Efficient Relational Querying of Software Structures, Proceedings of the 10th Working Conference on Reverse Engineering, p.216, November 13-17, 2003
• 4: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Robby, A Language Framework for Expressing Checkable Properties of Dynamic Software, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.205-223, August 30-September 01, 2000
• 6: S. Goldsmith, R. O'Callahan, and A. Aiken. Lightweight instrumentation from relational queries on program traces. Technical Report CSD-04-1315, UC Berkeley, 2004.
• 7: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 8: 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
• 9: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 10: T.A. Henzinger, R. Jhala, R. Majumdar, and M.A.A. Sanvido. Extreme model checking. In International Symposium on Verification: Theory and Practice, LNCS 2772, pages 332--358. Springer, 2003.
• 11: 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
• 12: Gerard J. Holzmann, Logic Verification of ANSI-C Code with SPIN, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.131-147, August 30-September 01, 2000
• 13: G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C.V. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In Proc. ECOOP, LNCS~1241, pages 220--242. Springer, 1997.
• 14: K. L. McMillan, A methodology for hardware verification using compositional model checking, Science of Computer Programming, v.37 n.1-3, p.279-309, May 2000 [doi>10.1016/S0167-6423(99)00030-1]
• 15: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 16: Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Reliability, Verification

Keywords:
software specification, software verification