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

[Vasilis Papavasileiou]

Another reminder: Philippe will give a talk at 1pm (166WVH). He
is already here despite the snowstorm.

Vasilis

On Mon, Jan 31, 2011 at 05:12:09PM -0500, Vasilis Papavasileiou wrote:
> 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