# Talk by Roland Glück (LTCS)

**Venue**

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

**Speaker**

Dr. Roland Glück (Deutsches Zentrum für Luft- und Raumfahrt)

**Title**

Towards Interactive Verification of Programmable Logic Controllers using Modal Kleene Algebra and KIV

**Abstract**

This talk introduces an approach to interactive verification of programmable logic controllers which often serve as controllers in safety critical systems and hence need thorough verification. It gives first a short introduction to programmable logic controllers, afterwards an introduction to the framework of modal Kleene Algebra and a short view of the interactive proving system KIV. Finally, it is shown how Kleene Algebra can be used to verify LTL properties of programmable logic controllers using the KIV system.

- Log in to post comments