Sándor, Levente (2018) Automatic Verification of Hoare Triples. Bachelor's Thesis, Computing Science.
|
Text
thesis.pdf Download (461kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (94kB) |
Abstract
This thesis presents an automatic proof generation system that can generate proofs for Hoare triples. The system works with an imperative, Pascal-like language similar to the one used in the course Program Correctness. In this language we can define assertions about the program state (boolean expressions) and commands (assignments). The system makes use of a knowledge base to avoid hard-coding arithmetic rules and operations. Given a precondition P , a series of assignments S, and a postcondition Q, the proof generator tries to find a proof for the Hoare triple {P }S{Q}. The possible outcomes can be: • valid: a resolution proof • invalid: a counterexample • undecided: the system did not find a proof nor a counter-example The output ”undecided” is necessary since it is fundamentally impossible to make a system that generates a proof or counter-example for each possible input.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Meijster, A. and Renardel de Lavalette, G.R. |
| Degree programme: | Computing Science |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 27 Jul 2018 |
| Last Modified: | 27 Jul 2018 12:20 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/18098 |
Actions (login required)
 |
View Item |