Abstract
It is now common to construct an extended static checker or software verification system using an SMT theorem prover as the underlying logical verifier. SMT provers have improved significantly in performance over the last several years. However, their usability as a component of software checking and verification systems still has gaps. This paper describes investigations in two areas: the reporting of counterexample information and the testing of vacuity, both of which are important to realistic use of such tools for typical software development. The use of solvers in verification is more effective if the solvers support minimal unsatisfiable cores and incremental construction, evolution and querying of satisfying assignments; current solvers only partially support these capabilities.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Flanagan C., Saxe J.B.: Avoiding exponential explosion: generating compact verification conditions. SIGPLAN Not. 36(3), 193–205 (2001)
Leino K.R.M.: Efficient weakest preconditions. Inform. Process. Lett. 93(6), 281–288 (2005)
Barrett C., de Moura L., Stump A.: Design and results of the 1st satisfiability modulo theories competition (SMT-COMP 2005). J. Autom. Reason. 35(4), 373–390 (2005)
The SMT-COMP web site provides results of the SMT competition and links to the system descriptions of the participants. http://smtcomp.org
Diller A.: Z: An Introduction to Formal Methods. 2nd edn. Wiley, New York (1994)
Meyer B.: Object-oriented Software Construction. Prentice Hall, New York, NY (1988)
Leavens G.T., Baker A.L., Ruby C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds) Behavioral Specifications of Businesses and Systems, pp. 175–188. Kluwer Academic Publishers, Boston (1999)
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML Reference Manual. Available from http://www.jmlspecs.org (May 2008)
JML web site. http://www.jmlspecs.org
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), vol. 3362 of Lecture Notes in Computer Science, pp. 49–69. Springer (2005)
Spec# web site. http://research.microsoft.com/SpecSharp
Luckham, D.C., von Henke, F.W., Krieg-Brückner, B., Owe, O.: ANNA—A Language for Annotating Ada Programs, Reference Manual, vol. 260 of Lecture Notes in Computer Science. Springer (1987)
ACSL web site. http://www.frama-c.cea.fr/acsl.html
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70. Microsoft Research (2005)
Why web site. http://why.lri.fr
The SMTLIB web site hosts benchmarks for SMT solvers and defines a common SMT input language. http://combination.cs.uiowa.edu/smtlib
Detlefs D., Nelson G., Saxe J.B.: Simplify: a theorem prover for program checking. J ACM 52(3), 365–473 (2005)
Rushby, J.: Tutorial: automated formal methods with PVS, SAL, and Yices. In: Fourth IEEE International Conference on Software Engineering and Formal Methods, 2006 (SEFM 2006), 11–15 September 2006
Yices web site. http://yices.csl.sri.com
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, Proceedings of 19th International Conference (CAV 2007) Berlin, Germany, 3–7 July 2007, vol. 4590 of Lecture Notes in Computer Science, pp 298–302. Springer (2007)
de Moura, L.M., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS, pp. 337–340 (2008)
Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference, Version 2.4. SRI International (2001)
Paulson, L.: Isabelle: A Generic Theorem Prover, vol. 828 of Lecture Notes in Computer Science. Springer (1994)
Cok, D.R., Kiniry, J.R.: ESC/Java2: uniting ESC/Java and JML: progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe, G., Burdy, L.,Huisman, M., Lanet, J.-L., Muntean, T. (eds.) Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004), vol. 3362 of Lecture Notes in Computer Science, pp. 108–128. Springer (2005)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer (2007)
KeY web site. http://www.key-project.org
Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Ernst, M.D., Jensen, T.P. (eds.) Program Analysis for Software Tools and Engineering (PASTE). ACM (September 2005)
Leino, K.R.M., Nelson, G., Saxe, J.B.: ESC/Java User’s Manual. Technical Note. Compaq Systems Research Center (October 2000)
CodeSonar® web site. http://www.grammatech.com/products/codesonar
Burdy, L., Requet, A., Lanet, J.-L.: Java Applet Correctness: A Developer-oriented Approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003: Formal Methods: International Symposium of Formal Methods Europe, vol. 2805 of Lecture Notes in Computer Science, pp. 422–439. Springer (2003)
Cook J.J.: Reverse Execution of Java Bytecode. Comput. J. 45, 2002 (2002)
Lewis, B.: Debugging Backwards in Time (2003)
Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical Report. Department of Computer Science, The University of Iowa (2006). Available at http://www.SMT-LIB.org
OpenJDK web site. http://openjdk.java.net
Beatty, D.L., Bryant, R.E.: Formally verifying a microprocessor using a simulation methodology. In: DAC ’94: Proceedings of the 31st Annual Conference on Design Automation, ACM, pp. 596–602. New York, NY, USA (1994)
Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: CAV ’97: Proceedings of the 9th International Conference on Computer Aided Verification, vol. 1254 of Lecture Notes in Computer Science, pp. 279–290. Springer, London, UK (1997)
Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS ’07: Proceedings of the 2007 Conference on Specification and Verification of Component-based Systems, ACM, pp. 23–30. New York, NY, USA (2007)
Egyed, A.: Instant consistency checking for the UML. In: ICSE ’06: Proceedings of the 28th International Conference on Software Engineering, ACM, pp. 381–390. New York, NY, USA (2006)
Smaragdakis, Y., Csallner, C., Subramanian, R.: Scalable satisfiability checking and test data generation from modeling diagrams. Autom. Softw. Eng. 16(1) (2009)
Leino, K.R.M., Moskal, M., Schulte, W.: Verification condition splitting. Available at http://research.microsoft.com/apps/pubs/default.aspx?id=77373 (2008)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Cok, D.R. Improved usability and performance of SMT solvers for debugging specifications. Int J Softw Tools Technol Transfer 12, 467–481 (2010). https://doi.org/10.1007/s10009-010-0138-x
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-010-0138-x