- Sandrine Blazy, David Pichardie, Alix Trieu.
Verified Constant-Time Implementations by Abstract Interpretation (extended version).
Journal of Computer Security, 27(1), January 2019, pp. 137-163.
- Sandrine Blazy, Rémi Hutin.
Formal verification of a program obfuscation based on mixed boolean-arithmetic expressions.
CPP 2019 - Certified Proofs and
Programs,
Lisbon, Portugal, 14-15/01/2019, ACM, pp.196-208.
- Sandrine Blazy, Marsha Chechik.
Selected Extended Papers of VSTTE 2016. Journal of Automated Reasoning, 60(3), 03/2018.
- Daniel Kästner, Ulrich Wünsche, Jörg Barrho, Marc Schlickling, Bernhard Schommer,
Michael Schmidt, Christian Ferdinand, Xavier Leroy, and Sandrine Blazy.
CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler.
Embedded Real Time Software and Systems (ERTS 2018). SEE, 01/2018.
- Sandrine Blazy, Pierre Castéran, Hugo Herbelin.
L'assitant de preuve Coq.
Techniques de l'ingénieur, August 2017.
- Frédéric Besson, Sandrine Blazy, Pierre Wilke.
CompCertS: a memory-aware verified C compiler using pointer as integer semantics.
ITP 2017,
8th Interactive Theorem Proving conference, Brasilia, Brazil, 26-29 September 2017.
Lecture Notes in Computer Science (LNCS) n°10499,
Springer, pp.81-97.
- Sandrine Blazy, David Pichardie, Alix Trieu.
Verified Constant-Time Implementations by Abstract Interpretation.
ESORICS 2017,
22nd European Symposium on Research in Computer Security, Oslo, 11-13 September 2017.
Lecture Notes in Computer Science (LNCS) n°10492,
Springer, pp. 260-277.
- Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu.
Verified Translation Validation of Static Analyses.
CSF 2017,
30th IEEE Computer Security Foundations Symposium, Santa Barbara, 21-25 August 2017.
pp. 405-419.
- Sandrine Blazy, David Bühler,
Boris Yakobowski. Structuring Abstract Interpreters through State and Value Abstractions.
VMCAI 2017,
18th International Conference on Verification, Model Checking and Abstract Interpretation, Paris, 22-24 January 2017.
Lecture Notes in Computer Science (LNCS) n°10145, Springer, pp. 112-130.
- Daniel Kästner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael Schmidt, Christian Ferdinand.
Closing the gap - The formally verified compiler CompCert.
25th Safety-critical Systems Symposium 2017 (SSS 2017),
Bristol, United Kingdom, 07/02/2017. CreateSpace, pp.163-180.
- Sandrine Blazy, Marsha Chechik.
Proceedings of
Verified Software: Theories, Tools, and Experiments-8th International Conference
(VSTTE 2016), Toronto, Canada, 17-18 July , 2016.
Lecture Notes in Computer Science 9971, Springer.
- Sandrine Blazy, Vincent Laporte, David Pichardie.
An Abstract Memory Functor for Verified C Static Analyzers.
ICFP'16 - 21st ACM SIGPLAN International Conference on Functional Programming,
Nara, Japan, pp. 325-337, 09/2016.
- Sandrine Blazy, Vincent Laporte,
David Pichardie.
Verified Abstract Interpretation Techniques
for Disassembling Low-level Self-Modifying Code. Extended
version, Journal of Automated Reasoning, 56(3), pp. 283-308,
03/2016.
- Sandrine Blazy, David Bühler,
Boris Yakobowski. Improving Static Analyses of C
Programs with Conditional Predicates. Science of
Computer Programming, volume 118, 03/2016,
pp. 77-95, Elsevier.
- Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard
Schommer, Markus Pister, Christian Ferdinand.
CompCert - A formally verified optimizing compiler
Embedded Real Time Software and
Systems (ERTS2 2016),
Toulouse, France, 27-29/01/2016. pp 188-195.
President's favorite award.
-
Sandrine Blazy, Alix Trieu.
Formal verification of control-flow flattening.
CPP 2016 - Certified Proofs and
Programs,
Saint Petersburg, USA, 18-19/01/2016, ACM, pp.176-187.
-
Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent.
Data tainting and Obfuscation: Improving Plausibility of Incorrect Taint.
15th conference on
Source Code Analysis and Manipulation, SCAM 2015, Bremen,
Germany, September 2015, IEEE, pp. 111-120.
- Sandrine Blazy, Thomas Jensen.
Proceedings of
the 22nd International
Static Analysis Symposium (SAS 2015),
Saint-Malo, France, 9-11 september, 2015. Lecture Notes in Computer Science 9291, Springer.
- Sandrine Blazy, Delphine Demange, David Pichardie.
Validating Dominator Trees for a Fast, Verified Dominance Test.
ITP-6th Interactive Theorem Proving conference, Nanjing, China, August 2015.
Lecture Notes in Computer Science (LNCS) n°9236,
Springer, pp.84-99.
- Frédéric Besson, Sandrine Blazy, Pierre Wilke.
A Concrete Memory Model for CompCert.
ITP-6th Interactive Theorem Proving conference, Nanjing, China, August 2015.
Lecture Notes in Computer Science (LNCS) n°9236,
Springer, pp.67-83.
- Jacques-Henri Jourdan, Vincent Laporte,
Sandrine Blazy, Xavier Leroy, David Pichardie. A formally C static analyzer.
42nd
Symposium on Principles on Programming
Languages, POPL 2015, Mumbai,
India, January 2015, ACM, pp. 247-259.
- Sandrine Blazy. Formal verification of compilers and
static analyzers. Programming Languages Mentoring Workshop,
PLMW@POPL 2015, Mumbai, India, 14/01/2015, pp.9, ACM.
- Sandrine Blazy, André Oliveria
Maroneze, David Pichardie. Verified validation of
program slicing.
CPP 2015 - Certified Proofs and
Programs,
Mumbai, India, January 2015, ACM, pp.109-117.
- Frédéric Besson, Sandrine Blazy, Pierre Wilke.
A Precise and Abstract Memory Model for C using
Symbolic Values.
12th
Asian
Symposium on Programming Languages and Systems, APLAS 2014.
Lecture Notes in Computer Science (LNCS) n°8858,
Springer, pp.449-468.
- Sandrine Blazy, David Bühler,
Boris Yakobowski. Improving Static Analyses of C
Programs with Conditional Predicates. Formal
Methods for Industrial Critical Systems, FMICS 2014,
19th international workshop on Formal Methods for Industrial Critical Systems.
Lecture Notes in Computer Science (LNCS) n°8718,
Springer, pp.140-154.
Best paper award.
- André Maroneze, Sandrine Blazy,
David Pichardie, Isabelle Puaut.
A Formally Verified WCET Estimation Tool.
14th International workshop on
worst-case execution time analysis, WCET
2014, Madrid, Spain, July 2014, pp. 11-20.
- Xavier Leroy, Andrew Appel, Sandrine Blazy, Gordon Stewart.
The CompCert memory model.
Cambridge University Press. 2014.
In Program Logics for Certified Compilers.
- Sandrine Blazy, Vincent Laporte,
David Pichardie.
Verified Abstract Interpretation Techniques
for Disassembling Low-level Self-Modifying Code. ITP-5th Interactive
Theorem Proving conference, Vienna, Austria, July 2014.
Lecture Notes in Computer Science (LNCS) n°8558,
Springer, pp.128-143.
- Sandrine Blazy,
Stéphanie Riaud. Measuring the robustness
of source program obfuscation. CODASPY 2014 - 4th
ACM Conference on Data and Application Security
and Privacy,
San Antonio, USA, March 2014, pp.123-126.
- Jael Kriener, Andy King, Sandrine Blazy. Proofs
you can believe in - Proving equivalences between Prolog
semantics in Coq. PPDP'13 - 15th International Symposium on Principles and Practice
of Declarative Programming, Madrid, Spain, September 2013.
ACM, pp.37-48.
- Sandrine Blazy, Christine Paulin-Mohring, David
Pichardie. Interactive
Theorem Proving conference (ITP 2013), Rennes, France,
July 2013. Lecture Notes in Computer Science (LNCS)
n°7998, Springer.
- Sandrine Blazy, Vincent Laporte,
André Maroneze, David Pichardie. Formal
verification of a C Value Analysis Based on
Abstract Interpretation. SAS - 20th Static
Analysis Symposium, Seattle, USA, June 2013.
Lecture Notes in Computer Science (LNCS) n°7935,
Springer, pp.324-344.
- Sandrine Blazy, André Maroneze, David
Pichardie. Formal
verification of Loop Bound Estimation for WCET
Analysis. VSTTE - Verified Software:
Theories, Tools and Experiments, Atherton, USA,
May 2013. Lecture Notes in Computer Science (LNCS)
n°8164, Springer, pp.281-303.
- Ricardo Bedin França, Sandrine
Blazy, Denis Favre-Félix, Xavier Leroy, Marc
Pantel, Jean Souyris. Formally verified optimizing
compilation in ACG-based flight control software.
ERTS2 2012: Embedded Real Time Software and
Systems, Toulouse, March 2012.
- Sandrine Blazy, Roberto Giaccobazzi. Towards an
obfuscating compiler. SSP 2012 - 2nd ACM SIGPLAN
Software Security and Protection Workshop,
Beijing, China, July 2012.
- Sandrine Blazy. Sémantiques
formelles. Habilitation à diriger des
recherches. Université d'Évry Val d'Essonne. 23
octobre 2008.
- Xavier Leroy, Sandrine Blazy. Formal
verification of a C-like memory model and its uses
for verifying program transformations. Journal
of Automated Reasoning. 41(1),
pp.1-31, July 2008.
- Sandrine Blazy.Which
C semantics to embed in the front-end of a formally
verified compiler?. TTVSI (Tools and
Techniques for Verification of System Infrastructure),
en l'honneur des 60 ans du professeur Michael
J.C.Gordon, Londres, 25-26 mars 2008.
- Benoît Robillard, Sandrine Blazy, Éric Soutif.Coloration avec
préférences : complexité, inégalités valides et
vérification formelle. ROADEF'08,
9e congrès de la Société Française de Recherche
Opérationnelle et d'Aide à la Décision,
Clermont-Ferrand, 25-27 février 2008, pp.123-138.
- Sandrine Blazy, Benoît Robillard, Éric Soutif. Vérification
formelle d'un algorithme d'allocation de registres
par coloration de graphes. Journées Françaises des
Langages Applicatifs (JFLA'08), Étretat, 26-29
janvier 2008, pp.31-46.
- Sandrine Blazy. Comment
gagner confiance en C ?. TSI, numéro spécial
"Langages applicatifs", Volume
26, numéro 9, 2007, pp.1195-1200.
- Sandrine Blazy, Benoît Robillard, Éric Soutif. Coloration
avec préférences dans les graphes triangulés.Journées
Graphes et algorithmes (JGA'07), Paris, 8-9
novembre 2007, p.32.
- Andrew W. Appel, Sandrine Blazy. Separation logic for
small-step Cminor. 20th Int. Conference on
Theorem Proving in Higher Order Logics (TPHOLs 2007),
Kaiserslautern, Germany 10-13 September 2007. LNCS
4732, pp.5-21.
- Sandrine Blazy. Experiments
in validating formal semantics for C. C/C++
Verification Workshop, Oxford, United Kingdom, 2
July 2007. Raboud University Nijmegen report
ICIS-R07015, pp.95-102.
- Andrew W.Appel, Sandrine Blazy.Separation logic for
small-step Cminor (extended version). INRIA
research report RR-6138,
March 2007, 29 pages.
Sandrine Blazy, Xavier Leroy.Formal verification of a
memory model for C-like imperative languages.
ICFEM'05: 7th Int. Conference on Formal Engineering
Methods, Manchester, UK, 1-4 November 2005. LNCS
3785, pp.280-299.
- Sandrine Blazy, Frédéric Gervais,
Régine Laleau. Une démarche outillée pour spécifier
formellement des patrons de conception réutilisables.
Workshop
Objets, Composants et Modèles dans l'ingénierie des
SI, associé à INFORSID'2003, Nancy, 3 juin 2003.
- Sandrine Blazy, Frédéric Gervais, Régine Laleau. Reuse of specification
patterns with the B method. ZB 2003
3rd Int. Conference of B and Z Users, Turku, Finland,
4-6 June 2003, LNCS
2651, pp.40-57.
- Sandrine Blazy, Frédéric Gervais,
Régine Laleau. Un exemple de réutilisation de patterns
de spécification avec la méthode B. Rapport technique
CEDRIC N°395.
- Sandrine Blazy. Transformations certifiées de
programmes impératifs. Rapport technique CEDRIC N°398.
- Sandrine Blazy. Specifying and
Automatically Generating a Specialization Tool for
Fortran 90.
Journal on Automated Software Engineering, Vol.7,
N°4, December 2000, pp.345-376.
- Stéphanie Bocs, Sandrine Blazy, P.Glaser, Claudine
Médigue. An automatic detection of prokaryotic CoDing
Sequences Combining Several Independant Methods.
Genome 2000, Int. Conf. on Microbial and Model
Genomes, Paris, 11-15 April 2000.
- Sandrine Blazy, Philippe Facon.
Interprocedural analysis for program comprehension by
specialization. 4th
IEEE Workshop on Program Comprehension, Berlin,
29-31 March 1996, pp.133-141.
- Sandrine Blazy, Philippe Facon. An automatic
interprocedural analysis for the understanding of
scientific application programs. Seminar on partial
evaluation, Dagsthul castle 12-16 February 1996, LNCS
1110, pp.1-16.
Sandrine Blazy, Philippe Facon. Formal specification and
prorotyping of a program specializer. TAPSOFT'95,
Aarhus, 22-26 May 1995, LNCS
915, pp.666-680.
- Sandrine Blazy, Philippe Facon. SFAC:
a tool for program comprehension by specialization.
3rd IEEE Workshop on Program Comprehension, Washington
D.C., 14-15 November 1994, pp.162-167.
- Sandrine Blazy, Philippe Facon. Partial evaluation
for the understanding of Fortran programs. Int.
Journal of Software Engineering and Knowledge
Engineering (IJSEKE), 4(4), December 1994,
pp.535-559.
- Sandrine Blazy, Philippe Facon Partial
evaluation as an aid to the comprehension of Fortran
programs. 2nd IEEE Workshop on Program Comprehension,
Capri, Italy, July 1993, pp.46-54.
- Sandrine Blazy, Philippe Facon Partial evaluation
for the understanding of Fortran programs. Software
Engineering and Knowledge Engineering (SEKE),
San Francisco, June 1993, pp.517-525. Awarded best
student paper.
- Sandrine Blazy, Philippe Facon Partial evaluation
and symbolic computation for the understanding of
Fortran programs. CAISE'93, Paris, June 1993, LNCS
685, pp.184-198.
- Sandrine Blazy La spécialisation de programmes pour
l'aide à la maintenance du logiciel. CNAM, 1993, PhD
thesis (in French).
- Marc Haziza, Jean-François Voidrot,
Earl Minor, Lech Pofelski, Sandrine Blazy. Software
maintenance: an analysis of industrial needs and
constraints. IEEE
Confrence Software Maintenance, Orlando, USA,
9-12 November 1992, pp.18-26.
- Sandrine Blazy, Philippe Facon. Évaluation partielle
pour la compréhension de programmes Fortran. Software
Engineering and its applications, Toulouse, December
1992, pp.411-417.