Program Verification as Satisfiability Modulo Theories

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 suitablefor many tasks that reduce to solving first-order formulas modulo theories.Here we propose to extend these benefits into the domain of symbolicsoftware model checking. We make a case that SMT-LIB canbe used, and to a limited extent adapted, for exchanging symbolicsoftware model checking benchmarks. We believe this layer facilitatesdividing innovations in modeling, developing program logics and front-ends,from developing algorithms for solving constraints over recursive predicates.