2 citations · 2 across the 4 of their papers we have counts for
4 papers
Verified Scalable Parallel Computing with Why3
Olivia Proust, Frédéric Loulergue
BSML is a pure functional library for the multi-paradigm language OCaml. BSML embodies the principles of the Bulk Synchronous Parallel (BSP) model, a model of scalable parallel com…
Towards Formal Verification of a TPM Software Stack
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue +2
The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack…
Experience Report: Teaching Code Analysis and Verification Using Frama-C
Salwa Souaf, Frédéric Loulergue
Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we pre…
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic a…