Damien Zufferey: From models and specifications to programs and constraints: increasing automation in verification

Abstract: Automated reasoning and verification tools have been developed to help programmers produce correct software.  However, the limit of decidability tells us that there is no silver bullet.  In this talk, I will show how we can harness the synergy between programming abstractions, formalisms, and verification methods to prove functional properties of complex system. First, I will speak about the verification of heap-manipulating programs. Separation logic (SL) has gained widespread popularity to specify such programs.  SL succinctly expresses how data structures are laid out in memory and its discipline of local reasoning mimics human intuition about proving heap programs correct.  Unfortunately, SL is a nonclassical logic and requires specialized provers.  We present a reduction of decidable SL fragments to a decidable first-order theory that fits into the satisfiability modulo theories (SMT) framework.  Our approach provides a way of integrating SL into verification tools with an SMT backend and combining SL fragments with other decidable first-order theories.

Then, I will shortly describe ongoing work about programming and verification of fault-tolerant distributed algorithms.  These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and faults. I will introduce PSync, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates faults. This high-level abstraction simplifies the implementation of fault-tolerant distributed algorithms, enables automated formal verification, and can be executed efficiently.

Bio:  Damien Zufferey is a Postdoctoral researcher in Martin Rinard's group at MIT  CSAIL since Octorber 2013. Before moving to MIT, He obtained a PhD at the  Institute of Science and Technology Austria (IST Austria) under supervision of Thomas A. Henzinger in September 2013 and a Master in computer science from EPFL in 2009. He is interested in improving software reliability by developing theoretical models, building analysis tools, and giving the programmer the appropriate language constructs. He is particularly interested in the study of complex concurrent systems. His research lies at the intersection of formal methods and programming languages.