Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People
Events

The Taub Faculty of Computer Science Events and Talks

On-the-fly Model Checking with Guided Abstraction
event speaker icon
Gal Sade (M.Sc. Thesis Seminar)
event date icon
Tuesday, 02.04.2019, 15:30
event location icon
Taub 601
event speaker icon
Advisor: Prof. O. Grumberg
Model checking is an automatic verification method that accepts a system model and a specification, and checks whether the model satisfies the specification. CTL is a branching temporal logic suitable for specifying behaviors of both software and hardware systems. In this work, we present a novel approach that combines on-the-fly verification with abstraction in order to obtain an efficient model checking. On-the-fly verification ensures that only parts that are needed for determining the satisfaction of the specification are developed. The abstraction is used to generalize information that was computed on fragments of the model, thus allowing the algorithm to halt without developing the entire model. We implemented our algorithm, compared it with a state-of-the-art CTL model checker and received very encouraging results.