Sandrine Blazy

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
A Fast Verified Liveness Analysis in SSA Form Automated Reasoning	2022-11-09	Paper
Verifying constant-time implementations by abstract interpretation	2022-08-25	Paper
\textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics Journal of Automated Reasoning	2019-08-21	Paper
A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data Journal of Automated Reasoning	2019-04-29	Paper
CompCertS: a memory-aware verified C compiler using pointer as integer semantics	2018-01-04	Paper
An abstract memory functor for verified C static analyzers Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming	2017-05-10	Paper
Verified abstract interpretation techniques for disassembling low-level self-modifying code Journal of Automated Reasoning	2016-05-26	Paper
A concrete memory model for CompCert Interactive Theorem Proving	2015-09-14	Paper
Validating dominator trees for a fast, verified dominance test Interactive Theorem Proving	2015-09-14	Paper
Verified abstract interpretation techniques for disassembling low-level self-modifying code Interactive Theorem Proving	2014-09-08	Paper
Program logics for certified compilers	2014-07-28	Paper
Formal verification of coalescing graph-coloring register allocation Programming Languages and Systems	2010-05-04	Paper
Mechanized semantics for the clight subset of the C language Journal of Automated Reasoning	2010-01-25	Paper
Formal verification of a C-like memory model and its uses for verifying program transformations Journal of Automated Reasoning	2008-09-10	Paper
Separation Logic for Small-Step cminor Lecture Notes in Computer Science	2008-09-02	Paper
scientific article; zbMATH DE number 2013574 (Why is no real title available?)	2003-12-04	Paper
Specifying and automatically generating a specialization tool for Fortran 90 Automated Software Engineering	2003-02-17	Paper

Research outcomes over time

This page was built for person: Sandrine Blazy