22nd ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE 2014), November 16–21, 2014, Hong Kong, China

Desktop Layout

Formal Methods and Verification
Main Research
Auditorium, Chair: Tevfik Bultan
Verifying CTL-Live Properties of Infinite State Models using an SMT Solver
Amirhossein Vakili and Nancy A. Day
(University of Waterloo, Canada)
Publisher's Version
Abstract: The ability to create and analyze abstract models is an important step in conquering software complexity. In this paper, we show that it is practical to verify dynamic properties of infinite state models expressed in a subset of CTL directly using an SMT solver without iteration, abstraction, or human intervention. We call this subset CTL-Live and it consists of the operators of CTL expressible using the least fixed point operator of the mu-calculus, which are commonly considered liveness properties (e.g., AF, AU). We show that using this method the verification of an infinite state model can sometimes complete more quickly than verifying a finite version of the model. We also examine modelling techniques to represent abstract models in first-order logic that facilitate this form of model checking.


Time stamp: 2020-07-05T15:02:52+02:00