Theory-Aided Model Checking of Concurrent Transition Systems

“Theory-Aided Model Checking of Concurrent Transition Systems” by Guy Katz, Clark Barrett, and David Harel. In Proceedings of the 15^th International Conference on Formal Methods In Computer-Aided Design (FMCAD '15), Sep. 2015, pp. 81-88. Austin, Texas.

Abstract

We present a method for the automatic compositional verification of certain classes of concurrent programs. Our approach is based on the casting of the model checking problem into a theory of transition systems within CVC4, a DPLL(T) based SMT solver. Our transition system theory then cooperates with other theories supported by the solver (e.g., arithmetic, arrays), which can help accelerate the verification process. More specifically, our theory solver looks for known patterns within the input programs and uses them to generate lemmas in the languages of other theories. When applicable, these lemmas can often steer the search away from safe parts of the search space, reducing the number of states to be explored and expediting the model checking procedure. We demonstrate the potential of our technique on a number of broad classes of programs.

BibTeX entry:

@inproceedings{KBH15,
   author = {Guy Katz and Clark Barrett and David Harel},
   title = {Theory-Aided Model Checking of Concurrent Transition Systems},
   booktitle = {Proceedings of the {\it 15^{th}} International Conference
	on Formal Methods In Computer-Aided Design (FMCAD '15)},
   pages = {81--88},
   publisher = {FMCAD Inc.},
   month = sep,
   year = {2015},
   note = {Austin, Texas},
   url = {http://theory.stanford.edu/~barrett/pubs/KBH15.pdf}
}

(This webpage was created with bibtex2web.)