אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

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.