29 septembre 2025
Paul Brunet (LACL)Computing devices and information systems have become ubiquitous. As their use broadens, a host of diverse requirements and considerations about their behaviours arise. This in turns creates a need for software analysis tools. In particular we are interested in techniques that are formal, static, and systematic.
Because of well-known impossibility results (e.g. Rice’s theorem), we cannot hope for a single “one-size-fits-all” approach. Indeed, as soon as a verification framework gets expressive enough, it become algorithmically intractable. The workaround is to rely instead on a variety of specialised analysis tools. The drawback is that any serious system analysis requires several such tools, and more often than not ends up developing ad-hoc variants of existing tools to better exploit the specifics of the system under study.
Therefore we believe new tools, models, and techniques for system analysis will continue being developed for the foreseeable future, in order to tackle new systems, new considerations, and new programming features. For these reasons, we want to provide better frameworks for building verification tools. More specifically, we are interested in ways to combine existing tools to produce new ones. Doing so, we wish to be able to derive the correctness of the composite tool from that of its constituting elements.
In this talk, I will propose such a framework, and argue it is able to capture a broad class of verification models, as well as useful proof techniques. This talk will be based on unpublished ongoing work.