Incremental SMT-based safety checking of reactive systems
Event details
| Date | 22.07.2013 |
| Hour | 16:15 › 17:15 |
| Speaker |
Prof. Cesare Tinelli 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, 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, and a Haifa Verification Conference award in 2010. He has given invited talks at 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 several conferences and workshops, and in the steering committees of CADE, IJCAR, FTP, FroCoS and SMT. He was the PC chair of FroCoS'11. |
| Location | |
| Category | Conferences - Seminars |
This talk presents a general approach and a corresponding parallel architecture for verifying safety properties of finite- and infinite-state reactive systems. The approach is based on reducing verification tasks to satisfiability problems in logics supported by modern Satisfiability Modulo Theories (SMT) solvers.
The architecture, implemented in the model checker Kind, is designed to accommodate the incorporation of automatic invariant generators to enhance the main verification algorithm based on k-induction. Furthermore, it allows the simultaneous incremental verification of multiple properties, where each proven property is immediately used to aid the verification of the remaining ones. The talk also briefly presents two general schemes for producing invariant generators for the architecture above. These schemes too rely on efficient SMT solvers and their ability to quickly generate counter-models of non-invariant conjectures.
The architecture, implemented in the model checker Kind, is designed to accommodate the incorporation of automatic invariant generators to enhance the main verification algorithm based on k-induction. Furthermore, it allows the simultaneous incremental verification of multiple properties, where each proven property is immediately used to aid the verification of the remaining ones. The talk also briefly presents two general schemes for producing invariant generators for the architecture above. These schemes too rely on efficient SMT solvers and their ability to quickly generate counter-models of non-invariant conjectures.
Practical information
- Informed public
- Free
Organizer
- Viktor Kuncak, Pierre-Emmanuel Cornilleau
Contact
- Pierre-Emmanuel Cornilleau