Paper Info
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.
Year
DOI
Venue
2015
10.1109/FMCAD.2015.7542252
FMCAD
Keywords
Field
DocType
SMT-based approach,fair termination analysis,coverability problem,safety checking,concurrent programs,coverability analysis,CAV14,Petri net analysis techniques,liveness properties,automata-theoretic approach,T-invariants,infinite computations
Programming language,Petri net,Computer science,Automaton,Real-time computing,Theoretical computer science,Software,Termination analysis,Concurrent computing,False positive paradox,Liveness,Executable
Conference
ISBN
Citations 
PageRank 
978-1-5090-4151-0
0
0.34
References 
Authors
26
2
Name
Order
Citations
PageRank
Javier Esparza11819147.63
Philipp Meyer2294.72