Analysis of Source Code Using UPPAAL

TL;DR

This paper proposes a method to analyze source code by bridging it with the Uppaal model checker using LLVM, enabling the application of Uppaal's strategy synthesis algorithms to source code analysis.

Contribution

It introduces a novel approach that connects source code with Uppaal via LLVM, facilitating advanced model checking techniques for software analysis.

Findings

Enables source code analysis using Uppaal's strategy synthesis.

Leverages LLVM as an intermediate language for integration.

Provides a practical bridge for applying model checking to real-world code.

Abstract

In recent years there has been a considerable effort in optimising formal methods for application to code. This has been driven by tools such as CPAChecker, DIVINE, and CBMC. At the same time tools such as Uppaal have been massively expanding the realm of more traditional model checking technologies to include strategy synthesis algorithms - an aspect becoming more and more needed as software becomes increasingly parallel. Instead of reimplementing the advances made by Uppaal in this area, we suggest in this paper to develop a bridge between the source code and the engine of Uppaal. Our approach uses the widespread intermediate language LLVM and makes recent advances of the Uppaal ecosystem readily available to analysis of source code.