|Title||From incorrectness logic proofs to violation witnesses|
Incorrectness logic is (a logic and associated) proof calculus for deductively showing the existence of program paths to errors. In automatic software verification, program paths to errors are encoded in so called violation witnesses. The task is to develop a method to connect incorrectness logic proofs with violation witnesses in a formal way.
- Incorrectness logic: http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/IncorrectnessLogic.pdf
- Violation witnesses: https://dl.acm.org/doi/pdf/10.1145/3477579
|Home institution||Department of Computing Science|
|Type of work||conceptual / theoretical|
|Type of thesis||Bachelor's|
|Author||Prof. Dr. Heike Wehrheim|