Theory-Aided model checking of concurrent transition systems

Guy Katz, Clark Barrett, David Harel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
EditorsRoope Kaivola, Thomas Wahl
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages81-88
Number of pages8
ISBN (Electronic)9780983567851
DOIs
StatePublished - Aug 11 2016
Event15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 - Austin, United States
Duration: Sep 27 2015Sep 30 2015

Publication series

NameProceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015

Other

Other15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
CountryUnited States
CityAustin
Period9/27/159/30/15

ASJC Scopus subject areas

  • Engineering (miscellaneous)
  • Computer Science Applications
  • Software

Fingerprint Dive into the research topics of 'Theory-Aided model checking of concurrent transition systems'. Together they form a unique fingerprint.

Cite this