Abstract
The SMT-LIB standard defines an input format and response requirements for Satisfiability-Modulo-Theories automated reasoning tools. The standard has been an incentive to improving and comparing the increasing supply of SMT solvers. It could also be more widely used in applications, providing a uniform interface and portability across different SMT tools. This tool paper describes a tutorial and accompanying software package, jSMTLIB, that will help users of SMT solvers understand and apply the newly revised SMT-LIB format; the tutorial also describes fine points of the SMT-LIB format which, along with a compliance suite, will be useful to SMT implementors. Finally, the tool suite includes adapters that allow using some older solvers, such as Simplify, as SMT-LIB compliant tools.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Barrett, C., Conway, C.: Leveraging SMT: Using SMT Solvers to Improve Verification; Using Verification to Improve SMT Solvers. Technical report, Department of Computer Science, New York University (2010)
Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the 3rd annual satisfiability modulo theories competition (SMT-COMP 2007). International Journal on Artificial Intelligence Tools (IJAIT) 17(4), 569–606 (2008)
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, England (2010)
Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa (2010)
Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Cok, D.: Improved usability and performance of SMT solvers for debugging specifications. International Journal on Software Tools for Technology Transfer (STTT) 12, 467–481 (2010); 10.1007/s10009-010-0138-x
de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Deters, M.: http://www.smtcomp.org/2010
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM 52(3), 365–473 (2005)
Dutertre, B., De Moura, L.: The yices SMT solver. Technical report (2006)
Griggio, A.: https://es.fbk.eu/people/griggio/misc/smtlib2parser.html
Hawkins, T.: http://hackage.haskell.org/package/smt-lib
Ranise, S., Tinelli, C.: The SMT-LIB Format: An Initial Proposal. In: Proceedings of the 1st Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Miami Beach, USA (2003)
Tinelli, C.: http://www.smt-lib.org
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cok, D.R. (2011). jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds) NASA Formal Methods. NFM 2011. Lecture Notes in Computer Science, vol 6617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20398-5_36
Download citation
DOI: https://doi.org/10.1007/978-3-642-20398-5_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20397-8
Online ISBN: 978-3-642-20398-5
eBook Packages: Computer ScienceComputer Science (R0)