Smten with satisfiability-based search
Abstract
Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) have been used in solving a wide variety of important and challenging problems, including automatic test generation, model checking, and program synthesis. For these applications to scale to larger problem instances, developers cannot rely solely on the sophistication of SAT and SMT solvers to efficiently solve their queries; they must also optimize their own orchestration and construction of queries. We present Smten, a high-level language for orchestrating and constructing satisfiability-based search queries. We show that applications developed using Smten require significantly fewer lines of code and less developer effort to achieve results comparable to standard SMT-based tools.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Oct 15, 2014
- Source ID
- 10.1145/2714064.2660208
Entities
People
- Nirav Dave
- Richard Uhler
Organizations
- Air Force Research Laboratory
- Defense Advanced Research Projects Agency
- Division of Computing and Communication Foundations
- SRI International