|Time+Place:||Sunday 20/12/2015 14:30 Room 337-8 Taub Bld.|
|Title:||Reasoning about Infinite-State Systems|
|Speaker:|| Sharon Shoham - CS-Lecture
|| Affiliation: || School of Computer Science at the Academic college of Tel Aviv-Yaffo
|| Host: || Orna Grumberg
Computerized systems are becoming an integral part of many aspects of our lives. Their correctness is therefore crucial. Many such systems have an infinite state space, resulting from an unbounded domain of variables, an unbounded size of a heap, an unbounded number of components, and so on. This makes checking the correctness of such systems hard, and in many cases undecidable. This talk will focus on verification of safety properties in infinite-state systems. We will first present a novel semi-algorithm, called Universal Property Directed Reachability (UPDR), for proving safety properties of infinite-state systems. UPDR proves safety by inferring inductive invariants in a universal fragment of first-order logic. UPDR terminates when it either discovers a counterexample to the safety property, infers an inductive universal invariant strong enough to establish the desired safety property, or finds a proof that such an invariant does not exist. We implemented an analyzer based on UPDR, and applied it to a collection of list-manipulating programs, as well as several distributed protocols. Our analyzer was able to automatically infer universal invariants strong enough to establish various safety properties, show the absence of such invariants for certain systems, and detect bugs. All of this, without the need for user-supplied abstraction predicates. We then address the more fundamental question of decidability of inferring inductive invariants in restricted fragments of first-order logic. We prove several decidability and undecidability results. Finally, we propose to tackle the undecidable fragments by an interactive approach for inference of universal inductive invariants. 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.