Colloquium - Compositional Program Verification using Max-SMT

Date: 
September 27, 2019 - 4:00pm to 5:00pm
Location: 
110 MLH
Speaker: 
Daniel Larraz

Recent developments on SMT solvers have become crucial to make program analysis techniques effective in practice. Despite their success, scalability is still an issue when applying these methods to large fragments of code. In order to address this problem, we propose a template-based (also known as constraint-based) approach using Max-SMT solvers. In particular, we present an automated compositional program verification technique for safety properties based on conditional inductive invariants. Our bottom-up program verification framework synthesizes and propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures when some precondition is not proved. In this talk we will provide an overview of the Max-SMT solving techniques and their application to safety verification and termination proving. These verification methods have successfully been implemented within the VeryMax tool which can check the correctness of C-like programs.

Bio

Daniel Larraz - UIowa CS PostDocDaniel Larraz is a postdoctoral researcher at the University of Iowa. His research focuses on the application of SMT-based techniques to the formal verification of computer systems. He is currently working with Prof. Cesare Tinelli on specification synthesis and verification of synchronous data-flow programs. He obtained his PhD from the Technical University of Catalonia (Barcelona, Spain) under the supervision of Prof. Albert Rubio. During his PhD, he worked on array invariant generation, termination analysis, and compositional safety verification of imperative programs using Max-SMT solvers. He also contributed to the implementation of the VeryMax tool, which has won the 1st prize in the categories of Integer Transition Systems and C Integer Programs of the International Termination Competition for several years. In 2014, he worked as a research intern at Microsoft Research Cambridge in the Programming Principles and Tools group under the supervision of Prof. Andrey Rybalchenko.