Theory-Aided model checking of concurrent transition systems

Guy Katz; Clark Barrett; David Harel

doi:10.1109/FMCAD.2015.7542256

Theory-Aided model checking of concurrent transition systems

Guy Katz, Clark Barrett, David Harel

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
Editors	Roope Kaivola, Thomas Wahl
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	81-88
Number of pages	8
ISBN (Electronic)	9780983567851
DOIs	https://doi.org/10.1109/FMCAD.2015.7542256
State	Published - Aug 11 2016
Event	15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 - Austin, United States Duration: Sep 27 2015 → Sep 30 2015

Publication series

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

Other

Other	15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015
Country/Territory	United States
City	Austin
Period	9/27/15 → 9/30/15

ASJC Scopus subject areas

Engineering (miscellaneous)
Computer Science Applications
Software

Access to Document

10.1109/FMCAD.2015.7542256

Cite this

Katz, G., Barrett, C., & Harel, D. (2016). Theory-Aided model checking of concurrent transition systems. In R. Kaivola, & T. Wahl (Eds.), Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 (pp. 81-88). Article 7542256 (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015). 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. ed. / Roope Kaivola; Thomas Wahl. Institute of Electrical and Electronics Engineers Inc., 2016. p. 81-88 7542256 (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Katz, G, Barrett, C & Harel, D 2016, Theory-Aided model checking of concurrent transition systems. in R Kaivola & T Wahl (eds), Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015., 7542256, Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, 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 Kaivola R, Wahl T, editors, 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. (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015). doi: 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. editor / Roope Kaivola ; Thomas Wahl. Institute of Electrical and Electronics Engineers Inc., 2016. pp. 81-88 (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015).

@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 = aug,

day = "11",

doi = "10.1109/FMCAD.2015.7542256",

language = "English (US)",

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

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "81--88",

editor = "Roope Kaivola and Thomas Wahl",

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

note = "15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 ; Conference date: 27-09-2015 Through 30-09-2015",

}

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

AN - SCOPUS:84985930297

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

SP - 81

EP - 88

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

A2 - Kaivola, Roope

A2 - Wahl, Thomas

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015

Y2 - 27 September 2015 through 30 September 2015

ER -

Theory-Aided model checking of concurrent transition systems

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this