[Pl-seminar] Reminder: Philippe Suter's Talk

[Vasilis Papavasileiou]

Reminder: Philippe's talk on Satisfiability Modulo Computable
Functions is tomorrow at 1pm, 166WVH. There are still meeting slots if
you are interested.

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