Computer Science Graduate Seminar: Verification of Embedded Software Models by Combining Abstract Interpretation, Symbolic Execution and Stability Analysis

Thursday, April 11, 2019, 10:00am

Location: Room 2202, Ahornstr. 55

Speaker: Christian Dernehl M.Sc. (i11)


In this talk, we present how embedded software models can be formally verified. Embedded software models often contain control application parts for which specific invariants can be derived. Together with abstract interpretation and symbolic execution, formal verification of control systems is feasible. Format verification is achieved by combining invariants derived from Lyapunov functions which are feed into sat-modulo theory solvers. The results are then used to prove formal requirements. This talk will be held in German.

The computer science lecturers invite interested people to join.