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