Sandrine Blazy
Sandrine Blazy
Professor of Computer Science, University of Rennes
Verified email at irisa.fr - Homepage
Title
Cited by
Cited by
Year
Formal verification of a C compiler front-end
S Blazy, Z Dargaye, X Leroy
International Symposium on Formal Methods, 460-475, 2006
2002006
Mechanized semantics for the Clight subset of the C language
S Blazy, X Leroy
Journal of Automated Reasoning 43 (3), 263-288, 2009
1882009
Formal verification of a C-like memory model and its uses for verifying program transformations
X Leroy, S Blazy
Journal of Automated Reasoning 41 (1), 1-31, 2008
1632008
Program logics for certified compilers
AW Appel
Cambridge University Press, 2014
1412014
A formally-verified C static analyzer
JH Jourdan, V Laporte, S Blazy, X Leroy, D Pichardie
ACM SIGPLAN Notices 50 (1), 247-259, 2015
1302015
Separation Logic for Small-Step cminor
AW Appel, S Blazy
International Conference on Theorem Proving in Higher Order Logics, 5-21, 2007
1242007
The CompCert memory model
X Leroy, AW Appel, S Blazy, G Stewart
602014
Reuse of specification patterns with the B method
S Blazy, F Gervais, R Laleau
International Conference of B and Z Users, 40-57, 2003
492003
Formal verification of a C value analysis based on abstract interpretation
S Blazy, V Laporte, A Maroneze, D Pichardie
International Static Analysis Symposium, 324-344, 2013
452013
Formal verification of a memory model for C-like imperative languages
S Blazy, X Leroy
International Conference on Formal Engineering Methods, 280-299, 2005
402005
Software maintenance: an analysis of industrial needs and constraints
M Haziza, JF Voidrot, JP Queille, L Pofelski, S Blazy
321992
CompCert-a formally verified optimizing compiler
X Leroy, S Blazy, D Kästner, B Schommer, M Pister, C Ferdinand
272016
Formally verified optimizing compilation in ACG-based flight control software
RB França, S Blazy, D Favre-Felix, X Leroy, M Pantel, J Souyris
262012
Formal verification of coalescing graph-coloring register allocation
S Blazy, B Robillard, AW Appel
European Symposium on Programming, 145-164, 2010
242010
Formal verification of loop bound estimation for WCET analysis
S Blazy, A Maroneze, D Pichardie
Working Conference on Verified Software: Theories, Tools, and Experiments …, 2013
222013
CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler
D Kästner, J Barrho, U Wünsche, M Schlickling, B Schommer, M Schmidt, ...
202018
A precise and abstract memory model for C using symbolic values
F Besson, S Blazy, P Wilke
Asian Symposium on Programming Languages and Systems, 449-468, 2014
202014
Verifying constant-time implementations by abstract interpretation
S Blazy, D Pichardie, A Trieu
Journal of Computer Security 27 (1), 137-163, 2019
192019
Partial evaluation for the understanding of Fortran programs
S Blazy, P Facon
International Journal of Software Engineering and Knowledge Engineering 4 …, 1994
191994
Closing the gap–the formally verified optimizing compiler CompCert
D Kästner, X Leroy, S Blazy, B Schommer, M Schmidt, C Ferdinand
172017
The system can't perform the operation now. Try again later.
Articles 1–20