Program Verification as Satisfiability Modulo Theories

9 pages•Published: August 19, 2013

Nikolaj Bjorner, Kenneth McMillan and Andrey Rybalchenko

Abstract

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 first-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 front-ends,
from developing algorithms for solving constraints over recursive predicates.

Keyphrases: program verification, smt, symbolic model checking

In: Pascal Fontaine and Amit Goel (editors). SMT 2012. 10th International Workshop on Satisfiability Modulo Theories, vol 20, pages 3-11.

Links:	https://easychair.org/publications/paper/qGkT
	https://doi.org/10.29007/1l7f

BibTeX entry

@inproceedings{SMT2012:Program_Verification_as_Satisfiability,
  author    = {Nikolaj Bjorner and Kenneth McMillan and Andrey Rybalchenko},
  title     = {Program Verification as Satisfiability Modulo Theories},
  booktitle = {SMT 2012. 10th International Workshop on Satisfiability Modulo Theories},
  editor    = {Pascal Fontaine and Amit Goel},
  series    = {EPiC Series in Computing},
  volume    = {20},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/qGkT},
  doi       = {10.29007/1l7f},
  pages     = {3-11},
  year      = {2013}}

Download PDF Open PDF in browser