BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Program Verification and Synthesis over Predicate Abstraction - Sa
 urabh Srivastava (visiting from UMD)
DTSTART:20090622T114500Z
DTEND:20090622T130000Z
UID:TALK18271@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Static determination of program correctness (verification) and
  automatic program construction (synthesis) are two important challenges i
 n programming languages research. Due to the undecidable nature of both pr
 oblems 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)\nsolvers. Very efficient SMT solvers a
 re now available and we use them to construct powerful verification techni
 ques. Verification can be accomplished by discovering appropriate invarian
 ts--facts that hold in every execution of the program.\n\nWe present three
  novel algorithms that discover sophisticated invariants using SMT solvers
 . Two of these algorithms use an iterative approach\, one computing the we
 akest invariants and the other the strongest invariants\, while the third 
 employs a constraint-based approach to encode the invariant as a SAT insta
 nce.\n\nWe have implemented the techniques developed under the umbrella pr
 oject\, Verification and Synthesis using SMT Solvers (VS3)\, in a tool by 
 the same name. Preliminary experiments using VS3 show promising\nresults. 
 In particular\, we discuss its power in verifying full correctness for all
  major sorting algorithms\, which are considered some of the most difficul
 t benchmarks for verification. Verifying full\ncorrectness for sorting alg
 orithms requires inferring \\forall\\exists invariants for permutation pro
 perties and \\forall invariants for sortedness properties.\n\nTime permitt
 ing\, we will briefly discuss a new principled approach to program synthes
 is that builds on program verification. We demonstrate encouraging prelimi
 nary results for program synthesis.\n\nProject Webpage http://www.cs.umd.e
 du/~saurabhs/pacs
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR