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, and applications of logic in computer
science. His research has been funded by the US National Science Foundation, the US Air
Force Office of Scientific Research, Intel Corporation, Rockwell Collins Incorporated,
and has appeared in more than 40 refereed publications. He has given invited talks at
such conferences as CAV, HVC, NFM, TABLEAUX, VERIFY, and WoLLIC.
He is a founder and leader of the SMT-LIB initiative, an international effort aimed at
standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers.
He was a co-recipient of the Haifa Verification Conference award in 2010 for his role
in building and promoting the SMT community, and of an NSF CAREER award in 2003. He has
served in the program committee of numerous automated reasoning conferences and workshops,
and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He was the PC chair
of FroCoS'11 and has been an associate editor of the Journal of Automated Reasoning
since 2007.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

This talk provides an overview of our current research on SMT-based model checking.
We present an incremental and parallel model checking architecture to verify safety
properties of synchronous systems. The architecture, implemented in the Lustre model
checker Kind, relies on SMT solvers as its main inference engines. It is designed
to minimize synchronization delays between subprocesses and accommodate the
incorporation of automatic auxiliary invariant generators to enhance the main
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 present a general scheme for instantiation-based invariant discovery
that can be used to implement invariant generators for the architecture above.
The scheme itself relies on efficient SMT solvers, and capitalizes on
their ability to quickly generate counter-models of non-invariant conjectures.
We discuss two specializations of the general scheme that make it feasible in
practice. Finally, we provide some experimental evidence showing how parallelism,
incrementality and invariant generation improve the speed and the precision of
the baseline k-induction algorithm.

Jennifer Müller

2900

--email hidden

passcode not visible

logged in users only