Stefan Ratschan

Date: 15:00, Tuesday, May 8, 2018
Speaker: Stefan Ratschan
Venue: IST Austria, Mondi 2

Time shifted to 3pm!

A common approach to solving problems in rigorous systems engineering is
to reduce them to constraint solving problems with a quantifier prefix
exists-forall. Here, the existential quantifier ranges over a
proof/certificate/program/controller to be found, and the universal
quantifier is used for specifying a property that the found object
should fulfill.

Recently, there has been a lot of work on algorithms for solving such
problems by iteratively learning the object to be found from concrete
counter-examples to the property. Many of those algorithms follow a
general scheme, often called counter-example guided inductive synthesis
(CEGIS). In the talk, we will present an algorithm of this type that
synthesizes certificates for safety of ordinary differential equations,
so-called barrier certificates.  We will draw general conclusions
regarding the usage of counter-example guided inductive synthesis in
continuous versus discrete structures.


Stefan Ratschan is a researcher at the Institute of Computer Science of
the Czech Academy of Sciences in Prague. He received his Ph.D. at the
Research Institute for Symbolic Computation at Johannes Kepler
University Linz, Austria, and has since then also been affiliated with
the University of Girona, Spain, and the Max-Planck-Institute for
Informatics, Saarbrücken, Germany. He currently heads the Department of
Computational Mathematics at the Institute of Computer Science of the
Czech Academy of Sciences.  The main scientific interests of Stefan
Ratschan are in the areas of formal verification of cyber-physical
systems and of constraint solving.

Posted in RiSE Seminar