University of Twente Student Theses

Login
As of Friday, 8 August 2025, the current Student Theses repository is no longer available for thesis uploads. A new Student Theses repository will be available starting Friday, 15 August 2025.

Loop Invariant Generation for Deductive Verification of Embedded Systems

Zambori, Ioan - Alexandru (2025) Loop Invariant Generation for Deductive Verification of Embedded Systems.

[img] PDF
904kB
Abstract:Embedded systems are highly specialized computer systems integrated within larger, typically electronic or mechanical systems. Unlike general computing on personal computers or enterprise servers, which aim to facilitate a vast set of operations applicable across many domains, embedded systems serve highly specific tasks and, as such, are generally purpose-built. Since embedded systems are present in safety-critical systems, suitable verification is paramount to ensure correctness. One strategy is the use of static analysis for deductive verification. VerCors is a toolset that can be used for such verification of concurrent systems, and previous work has generated tooling that can transform SystemC code into VerCors’ Prototypal Verification Language, alongside most of its respective annotations. This research aims to expand upon this work in the sector of loop invariant generation. This is achieved by simulating loop behavior and keeping track of over-approximations over the set of possible values of program variables. In doing so, we can provide numerical bounds for said program variables, which are used to provide invariants with respect to loop bounds.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:https://purl.utwente.nl/essays/107529
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page