MSc Defence by András Fekete

This thesis presents the design and implementation of a static analysis prototype tool for automatic error detection in a C#-inspired term language. Utilizing abstract interpretation as the foundational framework, we construct a prototype capable of detecting a set of targeted runtime exceptions, such as DivisionByZero, IndexOutOfBounds and UseOfUnassignedLocalVariable before execution. To achieve this, we formally define the syntax and structural semantics of this term language, alongside the corresponding abstract domains and semantics designed specifically to soundly capture the possible concrete behaviours of programs. We present soundness proofs, and reason about termination properties of this system to ensure safe over-approximation.

The implementation is built on top of the Microsoft .NET Compiler Platform SDK (Roslyn) to create the complete analysis pipeline. Initial experiments across a suite of synthetic sample programs demonstrate that the tool effectively detects potential runtime errors, automatically displaying the analysis results and exceptions alongside the source code within an integrated IDE extension.