News Archives

[Colloquium] Incremental SMT-based Safety Checking of Synchronous Systems

April 30, 2013

Watch Colloquium: 

M4V file (752 MB)

  • Date: Tuesday, April 30, 2013 
  • Time: 11:00 am — 12:30 pm 
  • Place: Mechanical Engineering 218

Cesare Tinelli
Dept. of Computer Science University of Iowa 

This talk provides an overview of our current research on automated verification. We present an incremental and parallel architecture for verifying safety properties of finite- and infinite-state synchronous systems. The architecture, implemented in the Lustre model checker Kind, relies on solvers for Satisfiability Modulo Theories (SMT) as its main inference engines. It is designed to accommodate the incorporation of automatic invariant generators to enhance Kind’s basic verification algorithm (k-induction). It also allows the verification of multiple properties incrementally and the use of proven input properties to aid the verification of the remaining ones. We also briefly discuss two general approaches we have developed to produce invariant generators for the architecture above. The schemes themselves rely on efficient SMT solvers and their ability to quickly generate counter-models of non-invariant conjectures.

Finally, we provide some experimental evidence showing how parallelism, incrementality and invariant generation improve the speed and the precision of our baseline k-induction algorithm, making Kind highly competitive with other infinite-state model checkers.

 

Bio: Cesare Tinelli is a professor of Computer Science and collegiate scholar at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, software verification, foundations of programming languages, and applications of logic in computer science.

His research has been funded by both governmental agencies (AFOSR, AFRL, NASA, NSF) and corporations (Intel, Rockwell Collins) and has appeared in more than 50 refereed publications. He has led the development of the award winning Darwin theorem prover and the Kind model checker, and co-led the development of the widely used CVC3 and CVC4 SMT solvers. He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers. He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, and a Haifa Verification Conference award in 2010 for his role in building and promoting the SMT community. He has given invited talks at such conferences as CAV, HVC, NFM, TABLEAUX, VERIFY, and WoLLIC.

He is an associate editor of the Journal of Automated Reasoning and a founder the SMT workshop series and the Midwest Verification Day series. He has served in the program committee of numerous automated reasoning and formal methods conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He was the PC chair of FroCoS’11.