Colloquium - Contract-based Compositional Verification of Infinite-State Reactive Systems

November 15, 2019 - 4:00pm to 5:00pm
110 MLH
Cesare Tinelli
University of Iowa

Model-based software development is a leading methodology for the construction of safety- and mission-critical embedded software systems. Formal models of such systems can be validated, via testing or formal verification, against system-level requirements and modified as needed before the actual system is built. In many cases, source code can be produced automatically from the model once the system designer is satisfied with it. As embedded systems become increasingly large and sophisticated, the size and complexity of models grows correspondingly. This makes the verification of system requirements harder, especially in the case of infinite-state systems. As with conventional software, contracts are an effective mechanism to establish boundaries between components in a system model, and can be used to aid the automated verification of system-level properties by means of compositional reasoning techniques. Component-level contracts also enable formal analyses that provide more accurate feedback for identifying sources of errors or the parts of a system that contribute to the satisfaction of a given requirement. This talk discusses our experience in designing an assume-guarantee-based contract language on top of the Lustre modeling language and leveraging it to extend the automated verifier Kind 2 with contract-based compositional reasoning techniques.


Cesare Tinelli portraitCesare Tinelli received a Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 1999 and is currently an F. Wendell Miller Professor in Computer Science at the University of Iowa. Professor Tinelli has done seminal work in automated reasoning, in particular in Satisfiability Modulo Theories (SMT), a field he helped establish through his research and service activities. His work has appeared in more than 80 refereed publications and has been funded both by governmental agencies (AFOSR, AFRL, DARPA, NASA, NSF, and ONR) and corporations (Amazon, Intel, General Electric, Rockwell Collins, and United Technologies). He is a founder and coordinator of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for SMT solvers. He has led the development of Kind 2, a model checker with users in the avionics and automotive industries. He has co-led the development of the widely used and award winning SMT solver CVC4. 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 more than 70 automated reasoning and formal methods conferences and workshops, as well as the steering committee of CADE, ETAPS, FTP, FroCoS, IJCAR, and SMT. He was the PC chair of FroCoS'11 and a PC co-chair of TACAS'15.