Explanations of Countercontractual Software Behaviour

Lead-Supervisor:

Can software explain its behaviour in faulty situations?

In this project, our overall objective is the explanation of countercontractual software behaviour, i.e., of software behaving differently than its specified contract. We aim at performing blame analyses determining the root cause of a contract violation (which component is faulty? which part of a contract is broken?). For this, we consider software verification techniques, proof calculi and formal specification of contracts.

Desirable background and expertise: Knowledge in software analysis and formal specification languages.