Advertisement

Journal of Automated Reasoning

, Volume 35, Issue 4, pp 373–390 | Cite as

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

  • Clark Barrett
  • Leonardo de Moura
  • Aaron Stump
Article

Abstract

The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.

Key words

competition decision procedures satisfiability modulo theories 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundation of Mathematics, pp. 102–103. North-Holland, Amsterdam (1954)Google Scholar
  2. 2.
    Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-based decision procedure for the boolean combination of difference constraints. In: The 7th International Conference on Theory and Applications of Satisfiability Testing (2004)Google Scholar
  3. 3.
    Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2), 140–164 (June 2003). Special Issue on the 12th International Conference on Rewriting Techniques and Applications (RTA 2001)MATHMathSciNetCrossRefGoogle Scholar
  4. 4.
    Barrett, C., Dill, D., Stump, A.: A framework for cooperating decision procedures. In: McAllester, D. (ed.) 17th International Conference on Automated Deduction, pp. 79–97. Springer, Berlin Heidelberg New York (2000)Google Scholar
  5. 5.
    Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: 14th International Conference on Computer-Aided Verification (2002)Google Scholar
  6. 6.
    Barrett, C.: Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D. thesis, Stanford University (2003)Google Scholar
  7. 7.
    Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification (CAV '04), vol. 3114 of Lecture Notes in Computer Science, pp. 515–518. Springer, Berlin Heidelberg New York (July 2004)Google Scholar
  8. 8.
    Barrett, C.W., Dill, D.L., Levitt, J.R.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) Proceedings of the 1st International Conference on Formal Methods In Computer-Aided Design (FMCAD '96), vol. 1166 of Lecture Notes in Computer Science, pp. 187–201. Springer, Berlin Heidelberg New York (November 1996)CrossRefGoogle Scholar
  9. 9.
  10. 10.
    Le Berre, D., Simon, L.: The essentials of the SAT 2003 Competition. In: Sixth International Conference on Theory and Applications of Satisfiability Testing, vol. 2919 of LNCS, pp. 452–467. Springer, Berlin Heidelberg New York (2003)Google Scholar
  11. 11.
    Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) 13th Conference on Computer-Aided Verification. Springer, Berlin Heidelberg New York (2001)Google Scholar
  12. 12.
    Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19(1), 7–34 (2001)MATHCrossRefGoogle Scholar
  13. 13.
    Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: Formal Methods in Computer-Aided Design. Springer, Berlin Heidelberg New York (November 2002)Google Scholar
  14. 14.
    Eén, N., Sörensson, N.: An extensible SAT-solver. In: Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), vol. 2919 of Lecture Notes in Computer Science, pp. 502–518. Springer, Berlin Heidelberg New York (May 2003)Google Scholar
  15. 15.
    Filliâtre, J., Owre, S., Rueß, H., Shankar, N.: ICS: Integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) 13th International Conference on Computer-Aided Verification, vol. 2102 of Lecture Notes in Computer Science, pp. 246–249. Springer, Berlin Heidelberg New York (2001)Google Scholar
  16. 16.
    Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. SIGPLAN Not. 37, 234–245 (2002)CrossRefGoogle Scholar
  17. 17.
    Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), vol. 3114 of Lecture Notes in Computer Science, pp. 175–188. Springer, Berlin Heidelberg New York (2004)Google Scholar
  18. 18.
    Lahiri, S., Bryant, R., Goel, A., Talupur, M.: Revisiting positive equality. In: Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of Lecture Notes in Computer Science, pp. 1–15. Springer, Berlin Heidelberg New York (2004)Google Scholar
  19. 19.
    Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Gupta, R. (ed.) ACM SIGPLAN Conference on Programming Language Design and Implementation (2003). Received best paper award.Google Scholar
  20. 20.
    Levitt, J.: Formal verification techniques for digital systems. Ph.D. thesis, Stanford University (1999)Google Scholar
  21. 21.
    Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.v., Schulz, S., Sebastiani, R., The MathSAT 3 System. In: Proceedings of the 20th International Conference on Automated Deduction (July 2005)Google Scholar
  22. 22.
    Möller, M., Rueß. H.: Solving bit-vector equations. In: Formal Methods in Computer-Aided Design, pp. 36–48 (1998)Google Scholar
  23. 23.
    Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV'05), Lecture Notes in Computer Science. Springer, Berlin Heidelberg New York (2005)Google Scholar
  24. 24.
    Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The development of CASC. AI Commun. 15(2–3), 79–90 (2002)MATHGoogle Scholar
  25. 25.
    Pnueli, A., Rodeh, Y., Strichman, O.: Range allocation for equivalence logic. In: 21st Conference on Foundations of Software Technology and Theoretical Computer Science, vol. 2245 of Lecture Notes in Computer Science, pp. 317–333. Springer, Berlin Heidelberg New York (2001)Google Scholar
  26. 26.
    Ranise, S., Tinellim, C.: The SMT-lib standard, version 1.1, 2005. Available from the “Documents” section of http://combination.cs.uiowa.edu/smtlib
  27. 27.
    Rueß, H., Shankar, N.: Solving linear arithmetic constraints. Technical Report SRI-CSL-04-01, SRI International (2004)Google Scholar
  28. 28.
    Seshia, S., Bryant, R.: Deciding quantifier-free presburger formulas using parameterized solution bounds. In: Logic in Computer Science. IEEE (2004)Google Scholar
  29. 29.
    Shankar, N.: Little engines of proof. Invited paper at Formal Methods Europe (2002)Google Scholar
  30. 30.
    Sheini, H.M., Sakallah, K.A.: A SAT-based decision procedure for mixed logical/integer linear problems. In: Barták, R., Milano, M. (eds.) CPAIOR, vol. 3524 of Lecture Notes in Computer Science, pp. 320–335. Springer, Berlin Heidelberg New York (2005)Google Scholar
  31. 31.
    Sheini, H.M., Sakallah, K.A.: A scalable method for solving satisfiability of integer linear arithmetic logic. In: Bacchus, F., Walsh, T., (eds.) SAT, vol. 3569 of Lecture Notes in Computer Science, pp. 241–256. Springer, Berlin Heidelberg New York (2005)Google Scholar
  32. 32.
    Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: 18th IEEE International Conference on Automated Software Engineering (2003). Received best paper awardGoogle Scholar
  33. 33.
    Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: 16th IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE Computer Society (2001)Google Scholar
  34. 34.
    Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) Proceedings of the 14th International Conference on Computer Aided Verification (CAV '02), vol. 2404 of Lecture Notes in Computer Science, pp. 500–504. Springer, Berlin Heidelberg New York (July 2002)Google Scholar
  35. 35.
    Velev, M., Bryant, R.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput. 35(2), 73–106 (February 2003)MATHMathSciNetCrossRefGoogle Scholar
  36. 36.
    Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) Proceedings of the 14th International Conference on Automated deduction, vol. 1249 of Lecture Notes in Artificial Intelligence, pp. 272–275. Springer, Berlin Heidelberg New York (July 1997)Google Scholar

Copyright information

© Springer Science+Business Media, Inc. 2006

Authors and Affiliations

  • Clark Barrett
    • 1
  • Leonardo de Moura
    • 2
  • Aaron Stump
    • 3
  1. 1.Department of Computer ScienceNew York UniversityNew YorkUSA
  2. 2.Computer Science LaboratorySRI InternationalMenlo ParkUSA
  3. 3.Department of Computer Science and EngineeringWashington University in St. LouisSt. LouisUSA

Personalised recommendations