Grunddaten
Titel | From incorrectness logic proofs to violation witnesses |
Beschreibung | 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 |
Heimateinrichtung | Department für Informatik |
Art der Arbeit | konzeptuell / theoretisch |
Abschlussarbeitstyp | Bachelor |
Autor | Prof. Dr. Heike Wehrheim |
Status | verfügbar |
Aufgabenstellung | |
Voraussetzung | |
Erstellt | 06.02.2023 |