Javascript must be enabled for the correct page display

Automatic Verification of Hoare Triples

Sándor, Levente (2018) Automatic Verification of Hoare Triples. Bachelor's Thesis, Computing Science.

[img]
Preview
Text
thesis.pdf

Download (461kB) | Preview
[img] 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:
Supervisor nameSupervisor E mail
Meijster, A.A.Meijster@rug.nl
Renardel de Lavalette, G.R.G.R.Renardel.de.Lavalette@rug.nl
Degree programme: Computing Science
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 27 Jul 2018
Last Modified: 27 Jul 2018 12:20
URI: http://fse.studenttheses.ub.rug.nl/id/eprint/18098

Actions (login required)

View Item View Item