Talk by Roland Glück (LTCS)

Short Title: 
Talk by Roland Glück
Event Date(s): 
Thursday, 30. November 2017 - 13:30

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

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

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

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.