Smten with satisfiability-based search
Smten with satisfiability-based search
复制标题
Smten 具有基于可满足性的搜索
DOI：
10.1145/2714064.2660208
复制
发表时间：
2014
影响因子：
--
通讯作者：
Nirav H. Dave
中科院分区：
文献类型：
--
作者：
R. Uhler;Nirav H. Dave
可满足性（SAT）和可满足性模理论（SMT）已被用于解决各种重要和具有挑战性的问题，包括自动测试生成，模型检测和程序综合。为了使这些应用程序能够扩展到更大的问题实例，开发人员不能仅仅依靠SAT和SMT求解器的复杂性来有效地解决他们的查询;他们还必须优化自己的查询编排和构造。我们提出了Smten，一个高层次的语言编排和构建满意度为基础的搜索查询。我们表明，使用Smten开发的应用程序需要显着更少的代码行和更少的开发人员的努力，以实现与标准的基于SMT的工具相比的结果。
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.
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G