An SMT-based Approach to Fair Termination Analysis.
FMCAD '15: Proceedings of the 15th Conference on Formal Methods in Computer-Aided Design(2015)
摘要
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.
更多查看译文
关键词
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
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络