Javascript must be enabled for the correct page display

Automatic Verification of Annotated Sequential Imperative Programs

Harmanny, Alinda (2020) Automatic Verification of Annotated Sequential Imperative Programs. Bachelor's Thesis, Computing Science.

[img]
Preview
Text
bCS_2020_HarmannyAJ.pdf

Download (562kB) | Preview
[img] Text
Toestemming.pdf
Restricted to Registered users only

Download (85kB)

Abstract

Writing error-free programs is a daunting task, and many programs contain several bugs that were not detected by the programmer. These undetected errors may cause a program to behave unexpectedly, crash, or produce incorrect results. To prevent such errors, a programmer may decide to prove the correctness of a program. However, producing these proofs is on itself an error-prone process. The aim of this project was to write a program that takes as its input an annotated program fragment and outputs a verdict for this annotation. The verdict can be ACCEPTED (which means that the annotation is correct), ERROR (in which case the program reports a counter-example disproving the correctness), or UNDECIDED (which means that the verification program was not able to prove the correctness of the annotation, nor did it find a counterexample). To prove an input program, we use a combination of expression simplification, resolution and unification.

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: 13 Aug 2020 07:10
Last Modified: 13 Aug 2020 07:10
URI: https://fse.studenttheses.ub.rug.nl/id/eprint/23070

Actions (login required)

View Item View Item