Loria Colloquium: Laura Kovács

The Loria is proud to announce a colloquium presentation by Laura Kovács on “Induction and synthesis in saturation-based theorem proving“.

Laura Kovács is a professor at the Faculty of Informatics of Vienna University of Technology (Vienna, Austria) and a leading researcher in the field of automated reasoning and symbolic computation.

Abstract:
Proof by induction is commonplace in mathematics. logic, formal verification, cybersecurity, and many more areas. This talk overviews recent progress in automating inductive reasoning in saturation-based first-order theorem proving We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. We also synthesize code that satisfies a given (inductive) logical specification, while proving the specification in a saturation-based framework.

 

The colloquium will take place at Loria’s amphitheater, on monday january 26th at 11:00 a.m.

People from outside the Loria must register by sending an email to Annabelle Chapron  –  annabelle.chapron (at) loria.fr  –  before January 23nd.