From Graphical Loop Invariants to Formal Verification

Abstract

Logic and mathematics are essential for understanding and verifying computer programs, yet many first-year computer science students struggle with these subjects. This Master’s thesis represents a first step toward automating the verification of simple C programs without requiring students to master formal logic. It demonstrates the feasibility of developing and implementing a tool that uses Loop Graph Invariants to verify computer programs written in C. To this end, a comprehensive process was developed and tested on ten programming problems covering the content of the introductory computer programming course taught at the University of Liège. All benchmarks were eventually verified. The methodology implemented relies on using the Dafny programming and verification language. It also involves a code translator that converts a C program into a program following the Dafny syntax, as well as an Embedding Model for French developed by La Javaness, used to extract the semantics of French sentences. Although the process is not fully automated, it paves the way for future research on the subject and the eventual realization of a complete system.