Book chapter
Smt-Switch: A Solver-Agnostic C++ API for SMT Solving
Theory and Applications of Satisfiability Testing – SAT 2021, pp.377-386
Lecture Notes in Computer Science, Springer International Publishing
07/02/2021
DOI: 10.1007/978-3-030-80223-3_26
Abstract
This paper presents Smt-Switch, an open-source, solver-agnostic API for SMT solving. Smt-Switch provides simple, uniform, and high-performance access to SMT solving for applications in areas such as automated reasoning, planning, and formal verification. It defines an abstract interface, which can be implemented by different SMT solvers. The interface allows the user to create, traverse, and manipulate terms, as well as dynamically dispatch queries to various underlying SMT solvers.
Details
- Title: Subtitle
- Smt-Switch: A Solver-Agnostic C++ API for SMT Solving
- Creators
- Makai Mann - Stanford UniversityAmalee Wilson - Stanford UniversityYoni Zohar - Stanford UniversityLindsey Stuntz - Stanford UniversityAhmed Irfan - Stanford UniversityKristopher Brown - Stanford UniversityCaleb Donovick - Stanford UniversityAllison Guman - Columbia UniversityCesare Tinelli - University of IowaClark Barrett - Stanford University
- Resource Type
- Book chapter
- Publication Details
- Theory and Applications of Satisfiability Testing – SAT 2021, pp.377-386
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-030-80223-3_26
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Publisher
- Springer International Publishing; Cham
- Language
- English
- Date published
- 07/02/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984259416202771
Metrics
65 Record Views