Representations
The formal analysis of automated systems is an important and growing industry. This activity routinely requires new verification frameworks to be developed to tackle new programming features, or new considerations (bugs of interest). Often, one particular property can prove frustrating to establish: completeness of the logic with respect to the semantics. In this paper, we try and make such developments easier, with a particular attention on completeness. Towards that aim, we propose a formal (meta-)model of software analysis systems (SAS), the eponymous Representations. This model requires few assumptions on the SAS being modeled, and as such is able to capture a large class of such systems. We then show how our approach can be fruitful, both to understand how existing completeness proofs can be structured, and to leverage this structure to build new systems and prove their completeness.
@inproceedings{b26,
title = "Representations",
author = "{Paul Brunet}",
year = 2026,
booktitle = "RAMiCS",
}
Related talks | ||
|
Séminaire du LACL
in Créteil,
September 2025
(in French)
.
|
More | |
|
Séminaire Plume
in Lyon,
June 2025.
|
More | |
|
Séminaire 68nqrt
in Rennes,
May 2025.
|
More | |
Related papers | ||
| On preorders (2025) | More | |