Supervisor:
How to explain software bugs?
In this project, our overall objective is the explanation of countercontractual software behaviour, i.e., of software behaving differently than its specified contract. To determine bugs in software, we employ software verification and logical satisfiability solvers. The topic of this PhD position is the explanation of software bugs to humans, i.e. to explain why a software exhibits countercontractual behaviour. For this, we intend to employ the results of automatic verifiers as well as proofs (of incorrectness) of proof calculi.
Desirable background and expertise: Knowledge in software analysis, formal specification languages, logics, Hoare-style proof calculi.