University of Cambridge > > Semantics Lunch (Computer Laboratory) > Program Verification and Synthesis over Predicate Abstraction

Program Verification and Synthesis over Predicate Abstraction

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

Static determination of program correctness (verification) and automatic program construction (synthesis) are two important challenges in programming languages research. Due to the undecidable nature of both problems no easy solutions are feasible. In this talk we present our work on program verification and synthesis, presenting techniques for both using Satisfiability Modulo Theory (SMT) solvers. Very efficient SMT solvers are now available and we use them to construct powerful verification techniques. Verification can be accomplished by discovering appropriate invariants—facts that hold in every execution of the program.

We present three novel algorithms that discover sophisticated invariants using SMT solvers. Two of these algorithms use an iterative approach, one computing the weakest invariants and the other the strongest invariants, while the third employs a constraint-based approach to encode the invariant as a SAT instance.

We have implemented the techniques developed under the umbrella project, Verification and Synthesis using SMT Solvers (VS3), in a tool by the same name. Preliminary experiments using VS3 show promising results. In particular, we discuss its power in verifying full correctness for all major sorting algorithms, which are considered some of the most difficult benchmarks for verification. Verifying full correctness for sorting algorithms requires inferring \forall\exists invariants for permutation properties and \forall invariants for sortedness properties.

Time permitting, we will briefly discuss a new principled approach to program synthesis that builds on program verification. We demonstrate encouraging preliminary results for program synthesis.

Project Webpage

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity