[Pl-seminar] Philippe Suter's Talk

[Vasilis Papavasileiou]

The title of the talk is "Satisfiability Modulo Computable Functions".

Vasilis

On Wed, Jan 26, 2011 at 07:00:09PM -0500, Vasilis Papavasileiou wrote:
> Philippe is visiting us on Tuesday, February 1st. He will give a talk
> at 1pm. This is hopefully the beginning of a seminar series on formal
> methods. Philippe will be available for meetings after 14:45. Please
> let me know if you would like to talk to him. An abstract follows:
> 
> Philippe Suter
> École Polytechnique Fédérale de Lausanne
> 
> Tuesday, 2/1
> 
> 1:00pm - 2:00pm
> Room 166WVH
> 
> We present an algorithm and the resulting system for reasoning about
> specifications over algebraic data types, integers and recursive
> functions. Our algorithm is capable of both 1) finding proofs and 2)
> generating concrete counterexamples. It interleaves these two
> complementary search activities using a fair search procedure. A high
> degree of automation comes in part from using the state-of-the-art SMT
> solver Z3.  We prove that our algorithm is terminating for a number of
> interesting classes of function specifications. (Because it doesn't
> need to recognize the input as belonging to any particular decidable
> fragment, it also succeeds for examples outside these fragments.) We
> have implemented our approach as a system to verify programs written
> in a purely functional subset of Scala. Using our system, we have
> verified a number of examples, such as syntax tree manipulations and
> functional data structure implementations. For incorrect properties,
> our system typically finds counterexample test cases quickly.
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar