Software and Computational Systems Lab

This topic is available as a BSc thesis, a MSc thesis, or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.

Goal: The safe interaction of computers with their physical environment (e.g. in modern car-controllers or care robots) requires utmost care as human health and life may be directly affected by a malfunction. Formal proofs provide a very high level of certainty about the safety of such cyber-physical systems. The dynamic logic of communicating hybrid programs (dLCHP), which describes interactions of computers, physical behavior, communication, and parallelism, is is a proof system supporting safety reasoning about cyber-physical systems.

In this thesis, parts of the theory of dLCHP are to be formalized in the interactive proof assistant Isabelle/HOL. That is, available pen-and-paper proofs are to be carried over into a mechanized theory in the proof assistant.

Requirements: The student must already have experience in using an interactive theorem prover (e.g. Isabelle/HOL, Coq, Lean), which might have been obtained in a lecture, seminar, or practical course.

This topic is available as a MSc thesis or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.

Goal: Uniform substitution is a proof rule that enables the implementation of a theorem prover kernel with very little code. For example, KeYmaera X, a theorem prover for reasoning about Cyber-physical systems, only has 2 kLOC code in its core, while its predecessor KeYmaera not using uniform substitution had 100 kLOC code.

Uniform substitution as a proof rule is always tailor-made for a certain logical system. In this thesis, uniform substitution for some logical system is to be investigated that is not considered yet. For example, uniform substitution could be studied for Incorrectness logic, which can be used for proving presence of bugs in software, or for separation logic, which can be used to reason about pointers.

Requirements: The student should have got good grades in logic and discrete structures and formal specification and verification

This topic is available as a BSc thesis, a MSc thesis, or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.

Goal: The safe interaction of computers with their physical environment (e.g. in modern car-controllers or care robots) requires utmost care as human health and life may be directly affected by a malfunction. Formal proofs provide a very high level of certainty about the safety of such cyber-physical systems. The dynamic logic of communicating hybrid programs (dLCHP), which describes interactions of computers, physical behavior, communication, and parallelism, is is a proof system supporting safety reasoning about cyber-physical systems.

In this thesis, the logic dLCHP is to be implemented as an extension of the interactive proof assistant KeYmaeara X for hybrid systems.

Requirements: The student should have experience in functional programming (e.g. Haskell, Scala) and modern web frameworks (e.g. Angular, React)

This topic is available as a MSc thesis, or as a MSc research training course with 6/12 ECTS. Mentoring is available in English and German.

Goal: Game logic with sabotage (GLs) [1] studies the abilities of competing agents to reach their goals if they can be so mean to lay traps for each other. Unlike game logic without sabotage, GLs is equiexpressive to the modal mu-calculus (L-mu), a logic that can be used to characterize important formal methods e.g. model checking. By equiexpresisvenss GLs provides a novel perspective onto these formal methods. Further, the equiexpressivenss is the foundation for the first completeness result for game logic. Recent flaws in related proofs make the formal verification of this proof a significant task.

In this thesis, the equiexpressivness of GLs and the L-mu is to be formalized in the proof assistant Isabelle/HOL.

Requirements: The student must already have experience in using an interactive theorem prover (e.g. Isabelle/HOL, Coq, Lean), which might have been obtained in a lecture, seminar, or practical course.