Page d'accueil // SnT // Distinguishe... // The Secrets of Automated Reasoning - November 28, 2013

The Secrets of Automated Reasoning - November 28, 2013

It is our pleasure to host this distinguished lecture by Prof. Christoph Weidenbach, Max Planck Institute for Informatics, Saarbruecken.

The lecture will be followed by a reception. Please feel free to forward this invitation.

Date: November 28, 2013
Time: 16:30
Venue: Weicker Building -Room B001 Ground floor, 4 rue Alphonse Weicker, L-2721 Luxembourg

Abstract: In the past decade there has been an enormous boost in the performance of automated reasoning procedures. They have made their way from academic research toys to standard industry tools. For example, SAT and SMT solvers are meanwhile indispensible in the hardware and software development process whereas first-order theorem provers greatly enhance the performance of verification tools.

While the old dream of automated reasoning in AI, where you simply describe a problem in a nice and easy declarative way and let the computer eventually solve it by generic methods, is still decades if not centuries away, for certain application areas, it has become true. For example, for ontologies, product models, automata, hybrid systems, security protocols, the very same automated reasoning technology can be used for analysis and verification, often outperforming special purpose algorithms.

In the talk I will reveal the main concepts behind this performace boost and I will give a forecast on what we can expect in future.

Christoph Weidenbach leads the "Automation of Logic Group" at the Max Planck Institute for Informatics and is Professor at the Computer Science department in Saarbruecken. He has also worked for several years as an IT manager in the car industry. He is a leading expert automated reasoning in general and one of the founders of the area of symbolic security protocol verification. In particular, he is the leader of the SPASS project, a family of automated reasoning tools covering a great variety of logics. Recently, he has launched a startup that transfers some results of his group into software used for product model analysis.