====== Artikel in Discrete Event Dynamic Systems ======
[[https://link.springer.com/article/10.1007%2Fs10626-019-00296-8|{{ :lehrstuhl:neuigkeiten:deds2020.jpg?nolink|}}]]
Wir freuen uns dass der Beitrag [[https://link.springer.com/article/10.1007%2Fs10626-019-00296-8|Leveraging Horn Clause Solving for Compositional Verification of PLC Software]] von [[lehrstuhl:mitarbeiter:bohlender|Dimitri Bohlender]] und [[lehrstuhl:mitarbeiter:kowalewski|Stefan Kowalewski]] im Journal //Discrete Event Dynamic Systems// publiziert wurde.

\\
Die Arbeit beschreibt wie SPS-Software mittels Horn Klauseln kompositional charakterisiert werden kann, um die formale Verifikation bisher herausfordernder Fragestellungen zu ermöglichen.
Insbesondere lässt sich die Charakterisierung mit den Ergebnissen vorhergehender statischer Analysen der einzelnen Softwarekomponenten kombinieren, um die Betrachtung von deren konkretem Verhalten soweit wie möglich zu vermeiden.