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.


Download (461kB) | Preview
[img] Text
Restricted to Registered users only

Download (94kB)


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

Actions (login required)

View Item View Item