26 citations · 35 across the 3 of their papers we have counts for
4 papers
Formally Verified Native Code Generation in an Effectful JIT -- or: Turning the CompCert Backend into a Formally Verified JIT Compiler
Aurèle Barrière, Sandrine Blazy, David Pichardie
Modern Just-in-Time compilers (or JITs) typically interleave several mechanisms to execute a program. For faster startup times and to observe the initial behavior of an execution,…
Formal Verification of a C Value Analysis Based on Abstract Interpretation
Sandrine Blazy, Vincent Laporte, André Maroneze +1
Static analyzers based on abstract interpretation are complex pieces of software implementing delicate algorithms. Even if static analysis techniques are well understood, their imp…
Separation Logic for Small-step Cminor
Andrew W. Appel, Sandrine Blazy
Cminor is a mid-level imperative programming language; there are proved-correct optimizing compilers from C to Cminor and from Cminor to machine language. We have redesigned Cminor…
Partial Evaluation for Program Comprehension
Sandrine Blazy
Program comprehension is the most tedious and time consuming task of software maintenance, an important phase of the software life cycle. This is particularly true while maintainin…