Program Verication as Satisability Modulo Theories
Nikolaj Bjrner, Ken L. McMillan, Andrey Rybalchenko · 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 rst-order formulas modulo theories. Here we propose to extend these benets 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.