BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Incremental SMT-based safety checking of reactive systems 
DTSTART:20130722T161500
DTEND:20130722T171500
DTSTAMP:20260601T173527Z
UID:cea735c1d3ecd195611fe8ef645fbe40fa1942d7a3bf4c37f9dd26d6
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Cesare Tinelli\nBio: Cesare Tinelli is a professor of Co
 mputer Science and collegiate scholar\nat the University of Iowa. He recei
 ved a PhD in Computer Science from the University of Illinois at Urbana-Ch
 ampaign in 1999. His research interests include automated reasoning\, form
 al methods\, and applications of logic in computer science.\nHis research 
 has been funded by both governmental agencies (AFOSR\, AFRL\,\nNASA\, NSF)
  and corporations (Intel\, Rockwell Collins) and has appeared\nin more tha
 n 50 refereed publications.\nHe has led the development of the award winni
 ng Darwin theorem prover and the Kind model checker\, and co-led the devel
 opment of the widely used CVC3 and CVC4 SMT solvers.\nHe is a founder and 
 coordinator of the SMT-LIB initiative\, an international effort aimed at s
 tandardizing benchmarks and I/O formats for Satisfiability Modulo Theories
  solvers. He received an NSF CAREER award in 2003\, and a Haifa Verificati
 on Conference award in 2010. He has given invited talks at CAV\, HVC\, NFM
 \, TABLEAUX\, VERIFY\, and WoLLIC. He is an associate editor of the Journa
 l of Automated Reasoning and a\nfounder the SMT workshop series and the Mi
 dwest Verification Day series.\nHe 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.\nThis t
 alk presents a general approach and a corresponding parallel architecture 
 for verifying safety properties of finite- and infinite-state reactive sys
 tems. The approach is based on reducing verification tasks to satisfiabili
 ty problems in logics supported by modern Satisfiability Modulo Theories (
 SMT) solvers.\nThe architecture\, implemented in the model checker Kind\, 
 is designed to accommodate the incorporation of automatic invariant gener
 ators to enhance the main verification algorithm based on k-induction. Fur
 thermore\, it allows the simultaneous incremental verification of multiple
  properties\, where each proven property is immediately used to aid the ve
 rification of the remaining ones. The talk also briefly presents two gener
 al schemes for producing invariant generators for the architecture above. 
 These schemes too rely on efficient SMT solvers and their ability to quick
 ly generate counter-models of non-invariant conjectures.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR