דלג לתוכן (מקש קיצור 's')
Logo of Technion
Logo of CS Department
אירועים

אירועים

On-the-fly Model Checking with Guided Abstraction
event speaker icon
Gal Sade, הרצאה סמינריונית למגיסטר
event date icon
יום ראשון, 20.12.2020, 16:00
event location icon
הרצאה באמצעות זום: https://technion.zoom.us/j/94459929157
event speaker icon
מנחה:  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.
[בחזרה לאינדקס האירועים]