EE Seminar: Tackling the State Explosion Problem in Model Checking
~~(The talk will be given in English)
Speaker: Dr. Sharon Shoham Buchbinder
School of Computer Sciences, Faculty of Exact Sciences, TAU
Monday, March 28th, 2016
15:00 - 16:00
Room 011, Kitot Bldg., Faculty of Engineering
Tackling the State Explosion Problem in Model Checking
Abstract
Model checking is an automated technique for checking whether a given system model satisfies a desired property, typically described as a temporal logic formula. As real models tend to be very big, model checking encounters the state-explosion problem. We present two approaches for tackling the state explosion problem in model checking.
First, we present a SAT-based technique for checking safety properties. Verification of safety properties is reducible to reachability analysis. We develop an algorithm which performs intertwined approximated forward and backward reachability analysis (DAR). The algorithm uses satisfiability checks and interpolation to overapproximate sets of reachable states.
Next, we consider compositional reasoning as a way for alleviating the state explosion problem. Compositional verification techniques aim to decompose the verification of a large system into the more manageable verification of its components. We develop a technique for automating circular assume-guarantee reasoning (ACR) in which the verification of individual components mutually depends on each other.
The talk is based on joint works with Karam Abd Elkader, Orna Grumberg, Corina Pasareanu, and Yakir Vizel.
Short Bio:
Sharon Shoham received a B.A. degree in Computer Science (summa cum laude) in 2001, a M.Sc. degree (cum laude) in 2004, and a Ph.D. degree in 2009, all from the Computer Science department of the Technion-Israel Institute of Technology. She holds a position as a senior lecturer in the school of Computer Science at the Academic college of Tel Aviv-Yaffo. She is currently on leave, visiting the programming languages group in Tel Aviv university.
