Speaker
Dr. Daniel Larraz, University of Iowa
Topic
Compositional Program Analysis Using Max-SMT
Abstract
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 I will provide an overview of the Max-SMT solving techniques and their application to compositional program analysis. These techniques have been implemented within the VeryMax tool which can check automatically safety and termination properties of C++ code.
Biography
Daniel 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 won in 2016 the 1st prize in the categories of Integer Transition Systems and C Integer Programs of the International Termination Competition. 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.
Invited by Professor Arie Gurfinkel.