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

Events

On-the-fly Model Checking with Guided Abstraction
event speaker icon
Gal Sade, M.Sc. Thesis Seminar
event date icon
Sunday, 20.12.2020, 16:00
event location icon
Zoom Lecture: https://technion.zoom.us/j/94459929157
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.
[Back to the index of events]