Time+Place: Sunday 20/12/2015 14:30 Room 337-8 Taub Bld.
Title: Reasoning about Infinite-State Systems
Speaker: Sharon Shoham - CS-Lecture http://www2.mta.ac.il/~sharon.shoham/
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.