Automatic Verification of Annotated Sequential Imperative Programs

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

Preview	Text bCS_2020_HarmannyAJ.pdf Download (562kB) | Preview
	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