Deriving a State Model of a Control Program by Symbolic Execution.

Thomas Bohm, Josef Pichler, Herbert Prähofer

Research output: Contribution to conferencePaperpeer-review


This paper presents an approach for deriving a state transition model which represents the behavior of a control component using symbolic execution. Symbolic execution is a technique for executing a program using symbolic values for unknowns. It explores execution paths in a program and then uses a SAT/SMT solver to prove that paths are feasible. Further, the approach allows using constraints on the environment and simplifications with a widening operator similar to abstract interpretation.We present the formal foundation of the approach, depict the the tool implementation, present results from a preliminary evaluation, and discuss various application scenarios.

Original languageEnglish
Number of pages6
Publication statusPublished - 24 Sept 2018


  • Program comprehension
  • Programmable logic controllers
  • State transition model
  • Symbolic execution


Dive into the research topics of 'Deriving a State Model of a Control Program by Symbolic Execution.'. Together they form a unique fingerprint.

Cite this