Nikolaj Bjorner, Kenneth L. McMillan, and Andrey Rybalchenko
30 June 2012
A key driver of SMT over the past decade has been an interchange format, SMT-LIB, and a growing set of benchmarks sharing this common format. SMT-LIB captures very well an interface that is suitable for many tasks that reduce to solving fifirst-order formulas modulo theories. Here we propose to extend these benefits into the domain of symbolic software model checking. We make a case that SMT-LIB can be used, and to a limited extent adapted, for exchanging symbolic software model checking benchmarks. We believe this layer facilitates dividing innovations in modeling, developing program logics and frontends, from developing algorithms for solving constraints over recursive predicates.
|Published in||10th International Workshop on Satisfiability Modulo Theories|