Formal Methods for Logic Control Software


This lecture teaches the basics and applications of static analysis and model checking in the domain of logic control software. To this end, common analyses and algorithms are applied to the cyclic execution model of programmable logic controllers. Topic are, among others:

  • The programming language Structured Text
    • Definition from IEC-61131-3
    • Formalisation as control flow graph
  • Static analysis
    • Data flow analysis
      • Order-theoretical foundations (Complete Lattice)
      • Live Variables Analysis
      • Reaching Definitions Analysis
      • Value Set Analysis
    • Program Dependency Graphs
    • Slicing
  • Abstract Interpretation
    • Galois Connections
    • Structural Operational Semantics
    • CEGAR-Variant for PLC State Space exploration
    • Relational Domains
  • Specification and Model Checking
    • CTL
    • Specification Automata
  • Logical Characterisation and Symbolic Reasoning
    • SMT encoding of Structured Text
    • Symbolic Execution
    • Large Block Encoding
    • Bounded Model Checking
    • IC3/PDR


The digital exercise class will take place every Friday from 10:30-12:00 via Zoom. See moodle for the link.

Lecture and exercise class

There will be voluntary exercise sheets published every week and solved in the exercise class. There will be recordings of the old lectures available in the moodle course room, and current recordings of the exercise class.



The contents of all lectures and exercise sheets will be relevant for the exam.



This website uses cookies. By using the website, you agree with storing cookies on your computer. If you do not agree please leave the website.More information about cookies

RWTH Aachen University - Chair of Computer Science 11 - Ahornstr. 55 - 52074 Aachen - Germany