Program Verification and Synthesis over Predicate Abstraction

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

• Saurabh Srivastava (visiting from UMD)
• Monday 22 June 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

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 http://www.cs.umd.edu/~saurabhs/pacs

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

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.