An SMT-based approach to fair termination analysis

Javier Esparza; Philipp J. Meyer

doi:10.1109/FMCAD.2015.7542252

An SMT-based approach to fair termination analysis

Javier Esparza, Philipp J. Meyer

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

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

7 Scopus citations

Abstract

Algorithms for the coverability problem have been successfully applied to safety checking for concurrent programs. In a former paper (An SMT-based Approach to Coverability Analysis, CAV14) we have revisited a constraint approach to coverability based on classical Petri net analysis techniques and implemented it on top of state-of-The-Art SMT solvers. In this paper we extend the approach to fair termination; many other liveness properties can be reduced to fair termination using the automata-Theoretic approach to verification. We use T-invariants to identify potential infinite computations of the system, and design a novel technique to discard false positives, that is, potential computations that are not actually executable. We validate our technique on a large number of case studies.

Original language	English
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	49-56
Number of pages	8
ISBN (Electronic)	9780983567851
DOIs	https://doi.org/10.1109/FMCAD.2015.7542252
State	Published - 11 Aug 2016
Event	15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 - Austin, United States Duration: 27 Sep 2015 → 30 Sep 2015

Publication series

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

Conference

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

Access to Document

10.1109/FMCAD.2015.7542252

Cite this

Esparza, J., & Meyer, P. J. (2016). An SMT-based approach to fair termination analysis. In R. Kaivola, & T. Wahl (Eds.), Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 (pp. 49-56). Article 7542252 (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.7542252

Esparza, Javier ; Meyer, Philipp J. / An SMT-based approach to fair termination analysis. 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. 49-56 (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015).

@inproceedings{5543e67e238b4f658ff095b77fb32aef,

title = "An SMT-based approach to fair termination analysis",

abstract = "Algorithms for the coverability problem have been successfully applied to safety checking for concurrent programs. In a former paper (An SMT-based Approach to Coverability Analysis, CAV14) we have revisited a constraint approach to coverability based on classical Petri net analysis techniques and implemented it on top of state-of-The-Art SMT solvers. In this paper we extend the approach to fair termination; many other liveness properties can be reduced to fair termination using the automata-Theoretic approach to verification. We use T-invariants to identify potential infinite computations of the system, and design a novel technique to discard false positives, that is, potential computations that are not actually executable. We validate our technique on a large number of case studies.",

author = "Javier Esparza and Meyer, {Philipp J.}",

note = "Publisher Copyright: {\textcopyright} 2015 FMCAD Inc.; 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015 ; Conference date: 27-09-2015 Through 30-09-2015",

year = "2016",

month = aug,

day = "11",

doi = "10.1109/FMCAD.2015.7542252",

language = "English",

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

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

pages = "49--56",

editor = "Roope Kaivola and Thomas Wahl",

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

}

Esparza, J & Meyer, PJ 2016, An SMT-based approach to fair termination analysis. in R Kaivola & T Wahl (eds), Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015., 7542252, Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, Institute of Electrical and Electronics Engineers Inc., pp. 49-56, 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, United States, 27/09/15. https://doi.org/10.1109/FMCAD.2015.7542252

An SMT-based approach to fair termination analysis. / Esparza, Javier; Meyer, Philipp J.
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. 49-56 7542252 (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015).

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

TY - GEN

T1 - An SMT-based approach to fair termination analysis

AU - Esparza, Javier

AU - Meyer, Philipp J.

PY - 2016/8/11

Y1 - 2016/8/11

N2 - Algorithms for the coverability problem have been successfully applied to safety checking for concurrent programs. In a former paper (An SMT-based Approach to Coverability Analysis, CAV14) we have revisited a constraint approach to coverability based on classical Petri net analysis techniques and implemented it on top of state-of-The-Art SMT solvers. In this paper we extend the approach to fair termination; many other liveness properties can be reduced to fair termination using the automata-Theoretic approach to verification. We use T-invariants to identify potential infinite computations of the system, and design a novel technique to discard false positives, that is, potential computations that are not actually executable. We validate our technique on a large number of case studies.

AB - Algorithms for the coverability problem have been successfully applied to safety checking for concurrent programs. In a former paper (An SMT-based Approach to Coverability Analysis, CAV14) we have revisited a constraint approach to coverability based on classical Petri net analysis techniques and implemented it on top of state-of-The-Art SMT solvers. In this paper we extend the approach to fair termination; many other liveness properties can be reduced to fair termination using the automata-Theoretic approach to verification. We use T-invariants to identify potential infinite computations of the system, and design a novel technique to discard false positives, that is, potential computations that are not actually executable. We validate our technique on a large number of case studies.

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

U2 - 10.1109/FMCAD.2015.7542252

DO - 10.1109/FMCAD.2015.7542252

M3 - Conference contribution

AN - SCOPUS:84985910515

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

SP - 49

EP - 56

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 -

Esparza J, Meyer PJ. An SMT-based approach to fair termination analysis. 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. 49-56. 7542252. (Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design, FMCAD 2015). doi: 10.1109/FMCAD.2015.7542252

An SMT-based approach to fair termination analysis

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this