metaSMT: Focus On Your Application Not On Solver Integration

Design and Implementation of Formal Tools and Systems 2011.

计算机科学;

Finn Haedicke Stefan Frehse Go¨rschwin Fey Daniel Große Rolf Drechsler

Others  :  http://ceur-ws.org/Vol-832/paper_5.pdf
PID  :  33668

学科分类：计算机科学（综合）

来源: CEUR

【 摘 要 】

Decision procedures are used as core technique in many applications today. In this context, automated reasoning based on Satisfiability Modulo Theories (SMT) is very effective. However, developers have to decide which concrete engine to use and how to integrate the engine into the application. Even if file formats like SMT- LIB standardize the input of many engines, advanced features remain unused and the integration of the engine is left to the programmer. This work presents metaSMT, a framework that inte- grates advanced reasoning engines into the program code of the respective application. metaSMT provides an easy to use language that allows engine independent programming while gaining from high performance reasoning engines. State-of-the-art solvers for satisfiability and other theories are available for the user via metaSMT with minimal programming effort. For two examples we show how metaSMT is used in current research projects.