Program Verification as Satisfiability Modulo Theories

Nikolaj Bjorner, Kenneth L. McMillan, and Andrey Rybalchenko


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.


Publication typeInproceedings
Published in10th International Workshop on Satisfiability Modulo Theories
> Publications > Program Verification as Satisfiability Modulo Theories