Huisman, Antal (2021) Translation Incorrectness and KAT. Bachelor's Thesis, Computing Science.
|
Text
bCS_2021_HuismanMA.pdf Download (271kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (129kB) |
Abstract
Hoare Logic is a propositional system that verifies if programs are correct. Recently a paper came out with Incorrectness Logic. Incorrectness Logic has a similar structure as Hoare Logic, but instead proves that a program contains an error or a bug. There is an Algebraic structure behind Hoare Logic named Kleene Algebra with Tests. With it, we can reduce proving a program correct with Hoare Logic into solving an equation in KAT. Is there also an Algebraic structure behind Incorrectness Logic? If so, we can similarly reduce finding an error into solving an equation. This report will explain the preliminaries of Hoare Logic, Incorrectness Logic and Kleene Algebra with Tests. Then it will detail the translation from Hoare Logic to KAT. We will find the translation from Incorrectness Logic to KAT and prove it is sound. Then we will discuss the difficulties into proving the translation correct.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Perez Parra, J.A. and Frumin, D. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 16 Jul 2021 10:39 |
| Last Modified: | 16 Jul 2021 10:39 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/25278 |
Actions (login required)
 |
View Item |