[Pl-seminar] Philippe Suter's Talk

[Vasilis Papavasileiou]

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.