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
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

Other

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

Fingerprint

Model checking
Surface mount technology
System theory
Casting

ASJC Scopus subject areas

  • Engineering (miscellaneous)
  • Computer Science Applications
  • Software

Cite this

Katz, G., Barrett, C., & Harel, D. (2016). Theory-Aided model checking of concurrent transition systems. In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 (pp. 81-88). [7542256] Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/FMCAD.2015.7542256

Theory-Aided model checking of concurrent transition systems. / Katz, Guy; Barrett, Clark; Harel, David.

Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015. Institute of Electrical and Electronics Engineers Inc., 2016. p. 81-88 7542256.

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

Katz, G, Barrett, C & Harel, D 2016, Theory-Aided model checking of concurrent transition systems. in Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015., 7542256, Institute of Electrical and Electronics Engineers Inc., pp. 81-88, 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, United States, 9/27/15. https://doi.org/10.1109/FMCAD.2015.7542256
Katz G, Barrett C, Harel D. Theory-Aided model checking of concurrent transition systems. In Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015. Institute of Electrical and Electronics Engineers Inc. 2016. p. 81-88. 7542256 https://doi.org/10.1109/FMCAD.2015.7542256
Katz, Guy ; Barrett, Clark ; Harel, David. / Theory-Aided model checking of concurrent transition systems. Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 81-88
@inproceedings{24001341dbcf44ea9ba8d4bdd1cfb3ae,
title = "Theory-Aided model checking of concurrent transition systems",
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.",
author = "Guy Katz and Clark Barrett and David Harel",
year = "2016",
month = "8",
day = "11",
doi = "10.1109/FMCAD.2015.7542256",
language = "English (US)",
pages = "81--88",
booktitle = "Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
address = "United States",

}

TY - GEN

T1 - Theory-Aided model checking of concurrent transition systems

AU - Katz, Guy

AU - Barrett, Clark

AU - Harel, David

PY - 2016/8/11

Y1 - 2016/8/11

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84985930297&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84985930297&partnerID=8YFLogxK

U2 - 10.1109/FMCAD.2015.7542256

DO - 10.1109/FMCAD.2015.7542256

M3 - Conference contribution

SP - 81

EP - 88

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

PB - Institute of Electrical and Electronics Engineers Inc.

ER -