Topic: From incorrectness logic proofs to violation witnesses

Topic: From incorrectness logic proofs to violation witnesses

Personal details

Title From incorrectness logic proofs to violation witnesses
Description
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.

References:
- 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
Status available
Problem statement
Requirement
Created 06/02/23

Study data

Departments
  • Formale Methoden
Degree programmes
  • Bachelor's Programme Computing Science
Assigned courses
Contact person