Theory and practice of automated theorem proving

Monika Seisenberger, Swansea University. Part of the Algebra, Logic and Algorithms seminar series.

In this talk we look at automated theorem proving and its application to an industrial context, the railway domain.  In the first part we briefly summarize how we have generated an SAT solver, which we extracted from a formal constructive proof of the completeness of the Davis-Putnam-Logemann-Loveland (DPLL) proof system, and how it is applied in the verification of a railway control system.  The technique can be further extended to build a resolution solver or allow optimisations such as clause learning.  In the second part, we report on the modelling and verification of the European Rail Traffic Management System (ERTMS), carried out in Real-Time Maude.  The techniques used are simulation (by error injection) and model-checking.  We also argue why our analysis by model-checking is complete, i.e. guarantees safety at all times.