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


On-the-fly Model Checking with Guided Abstraction
event speaker icon
Gal Sade, M.Sc. Thesis Seminar
event date icon
Monday, 21.12.2020, 16:00
event location icon
Zoom Lecture:
event speaker icon
Advisor:  Prof. Orna 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.
[Back to the index of events]