Automatic Verification of Annotated Sequential Imperative Programs
Alinda Harmanny · 2020
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.