Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
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