default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSandrine Blazy
Person information
- affiliation: INRIA, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[c43]Sandrine Blazy
:
From Mechanized Semantics to Verified Compilation: the Clight Semantics of CompCert. FASE 2024: 1-21- [e4]Amin Timany, Dmitriy Traytel, Brigitte Pientka, Sandrine Blazy:
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024. ACM 2024 [contents] - 2023
- [j16]Aurèle Barrière, Sandrine Blazy, David Pichardie:
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. Proc. ACM Program. Lang. 7(POPL): 249-277 (2023) - [c42]Sandrine Blazy:
CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote). CPP 2023: 1 - [c41]Yann Herklotz, Delphine Demange, Sandrine Blazy:
Mechanised Semantics for Gated Static Single Assignment. CPP 2023: 182-196 - 2022
- [i8]Aurèle Barrière, Sandrine Blazy, David Pichardie:
Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert Backend into a Formally Verified JIT Compiler. CoRR abs/2212.03129 (2022) - 2021
- [j15]Aurèle Barrière, Sandrine Blazy, Olivier Flückiger, David Pichardie, Jan Vitek:
Formally verified speculation and deoptimization in a JIT compiler. Proc. ACM Program. Lang. 5(POPL): 1-26 (2021) - [c40]Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie:
Secure Compilation of Constant-Resource Programs. CSF 2021: 1-12 - 2020
- [j14]Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL): 7:1-7:30 (2020) - [c39]Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie:
A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) 2020: 324-340 - [c38]Sandrine Blazy:
From Verified Compilation to Secure Compilation: a Semantic Approach. PLAS@CCS 2020: 1
2010 – 2019
- 2019
- [j13]Frédéric Besson, Sandrine Blazy, Pierre Wilke:
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data. J. Autom. Reason. 62(4): 433-480 (2019) - [j12]Frédéric Besson, Sandrine Blazy, Pierre Wilke:
CompCertS: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics. J. Autom. Reason. 63(2): 369-392 (2019) - [j11]Sandrine Blazy, David Pichardie, Alix Trieu:
Verifying constant-time implementations by abstract interpretation. J. Comput. Secur. 27(1): 137-163 (2019) - [c37]Sandrine Blazy, Rémi Hutin:
Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. CPP 2019: 196-208 - [c36]Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, Pierre Wilke:
Compiling Sandboxes: Formally Verified Software Fault Isolation. ESOP 2019: 499-524 - [c35]Sandrine Blazy:
Teaching Deductive Verification in Why3 to Undergraduate Students. FMTea 2019: 52-66 - [i7]Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019: 926 (2019) - 2018
- [j10]Sandrine Blazy, Marsha Chechik:
Selected Extended Papers of VSTTE 2016. J. Autom. Reason. 60(3): 255-256 (2018) - 2017
- [c34]Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu:
Verified Translation Validation of Static Analyses. CSF 2017: 405-419 - [c33]Sandrine Blazy, David Pichardie, Alix Trieu:
Verifying Constant-Time Implementations by Abstract Interpretation. ESORICS (1) 2017: 260-277 - [c32]Frédéric Besson, Sandrine Blazy, Pierre Wilke:
CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. ITP 2017: 81-97 - [c31]Sandrine Blazy, David Bühler, Boris Yakobowski:
Structuring Abstract Interpreters Through State and Value Abstractions. VMCAI 2017: 112-130 - 2016
- [j9]Sandrine Blazy, Vincent Laporte, David Pichardie:
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. J. Autom. Reason. 56(3): 283-308 (2016) - [j8]Sandrine Blazy, David Bühler, Boris Yakobowski:
Improving static analyses of C programs with conditional predicates. Sci. Comput. Program. 118: 77-95 (2016) - [c30]Sandrine Blazy, Alix Trieu:
Formal verification of control-flow graph flattening. CPP 2016: 176-187 - [c29]Sandrine Blazy, Vincent Laporte, David Pichardie:
An abstract memory functor for verified C static analyzers. ICFP 2016: 325-337 - [e3]Sandrine Blazy, Marsha Chechik:
Verified Software. Theories, Tools, and Experiments - 8th International Conference, VSTTE 2016, Toronto, ON, Canada, July 17-18, 2016, Revised Selected Papers. Lecture Notes in Computer Science 9971, 2016, ISBN 978-3-319-48868-4 [contents] - 2015
- [c28]Sandrine Blazy, André Maroneze, David Pichardie:
Verified Validation of Program Slicing. CPP 2015: 109-117 - [c27]Frédéric Besson, Sandrine Blazy, Pierre Wilke:
A Concrete Memory Model for CompCert. ITP 2015: 67-83 - [c26]Sandrine Blazy, Delphine Demange, David Pichardie:
Validating Dominator Trees for a Fast, Verified Dominance Test. ITP 2015: 84-99 - [c25]Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie:
A Formally-Verified C Static Analyzer. POPL 2015: 247-259 - [c24]Sandrine Blazy, Stéphanie Riaud, Thomas Sirvent:
Data tainting and obfuscation: Improving plausibility of incorrect taint. SCAM 2015: 111-120 - [e2]Sandrine Blazy, Thomas P. Jensen:
Static Analysis - 22nd International Symposium, SAS 2015, Saint-Malo, France, September 9-11, 2015, Proceedings. Lecture Notes in Computer Science 9291, Springer 2015, ISBN 978-3-662-48287-2 [contents] - [i6]Sandrine Blazy:
Formal verification of compilers and static analyzers. PLMW@POPL 2015: 9:1 - 2014
- [c23]Frédéric Besson, Sandrine Blazy, Pierre Wilke:
A Precise and Abstract Memory Model for C Using Symbolic Values. APLAS 2014: 449-468 - [c22]Sandrine Blazy, Stéphanie Riaud:
Measuring the robustness of source program obfuscation: studying the impact of compiler optimizations on the obfuscation of C programs. CODASPY 2014: 123-126 - [c21]Sandrine Blazy, David Bühler, Boris Yakobowski:
Improving Static Analyses of C Programs with Conditional Predicates. FMICS 2014: 140-154 - [c20]Sandrine Blazy, Vincent Laporte, David Pichardie:
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. ITP 2014: 128-143 - [c19]André Maroneze, Sandrine Blazy, David Pichardie, Isabelle Puaut:
A Formally Verified WCET Estimation Tool. WCET 2014: 11-20 - 2013
- [c18]Jael Kriener, Andy King, Sandrine Blazy:
Proofs you can believe in: proving equivalences between Prolog semantics in Coq. PPDP 2013: 37-48 - [c17]Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie:
Formal Verification of a C Value Analysis Based on Abstract Interpretation. SAS 2013: 324-344 - [c16]Sandrine Blazy, André Maroneze, David Pichardie:
Formal Verification of Loop Bound Estimation for WCET Analysis. VSTTE 2013: 281-303 - [e1]Sandrine Blazy, Christine Paulin-Mohring, David Pichardie:
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings. Lecture Notes in Computer Science 7998, Springer 2013, ISBN 978-3-642-39633-5 [contents] - [i5]Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie:
Formal Verification of a C Value Analysis Based on Abstract Interpretation. CoRR abs/1304.3596 (2013) - 2011
- [j7]Sandrine Blazy:
Introduction. Tech. Sci. Informatiques 30(4): 369-370 (2011) - 2010
- [c15]Sandrine Blazy, Benoît Robillard, Andrew W. Appel:
Formal Verification of Coalescing Graph-Coloring Register Allocation. ESOP 2010: 145-164
2000 – 2009
- 2009
- [j6]Sandrine Blazy, Xavier Leroy:
Mechanized Semantics for the Clight Subset of the C Language. J. Autom. Reason. 43(3): 263-288 (2009) - [c14]Sandrine Blazy, Benoît Robillard:
Live-range unsplitting for faster optimal coalescing. LCTES 2009: 70-79 - [i4]Sandrine Blazy, Xavier Leroy:
Mechanized semantics for the Clight subset of the C language. CoRR abs/0901.3619 (2009) - 2008
- [b1]Sandrine Blazy:
Sémantiques formelles. (Formal semantics). University of Évry Val d'Essonne, France, 2008 - [j5]Xavier Leroy, Sandrine Blazy:
Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations. J. Autom. Reason. 41(1): 1-31 (2008) - 2007
- [j4]Sandrine Blazy:
Chronique : Comment gagner la confiance en C? Tech. Sci. Informatiques 26(9): 1195-1200 (2007) - [c13]Andrew W. Appel, Sandrine Blazy:
Separation Logic for Small-Step cminor. TPHOLs 2007: 5-21 - [i3]Andrew W. Appel, Sandrine Blazy:
Separation Logic for Small-step Cminor. CoRR abs/0707.4389 (2007) - 2006
- [c12]Sandrine Blazy, Zaynah Dargaye, Xavier Leroy:
Formal Verification of a C Compiler Front-End. FM 2006: 460-475 - [i2]Sandrine Blazy:
Partial Evaluation for Program Comprehension. CoRR abs/cs/0610096 (2006) - [i1]Sandrine Blazy, Frédéric Gervais, Régine Laleau:
Reuse of Specification Patterns with the B Method. CoRR abs/cs/0610097 (2006) - 2005
- [c11]Sandrine Blazy, Xavier Leroy:
Formal Verification of a Memory Model for C-Like Imperative Languages. ICFEM 2005: 280-299 - 2003
- [c10]Sandrine Blazy, Frédéric Gervais, Régine Laleau:
Reuse of Specification Patterns with the B Method. ZB 2003: 40-57 - 2000
- [j3]Sandrine Blazy:
Specifying and Automatically Generating a Specialization Tool for Fortran 90. Autom. Softw. Eng. 7(4): 345-376 (2000)
1990 – 1999
- 1998
- [j2]Sandrine Blazy, Philippe Facon:
Partial Evaluation for Program Comprehension. ACM Comput. Surv. 30(3es): 17 (1998) - 1997
- [c9]Sandrine Blazy, Philippe Facon:
Application of Formal Methods to the Development of a Software Maintenance Tool. ASE 1997: 162-171 - 1996
- [c8]Sandrine Blazy, Philippe Facon:
An Automatic Interprocedural Analysis for the Understanding of Scientific Application Programs. Dagstuhl Seminar on Partial Evaluation 1996: 1-16 - [c7]Sandrine Blazy, Philippe Facon:
Interprocedural analysis for program comprehension by specialization. WPC 1996: 133- - 1995
- [c6]Sandrine Blazy, Philippe Facon:
Formal Specification and Prototyping of a Program Specializer. TAPSOFT 1995: 666-680 - 1994
- [j1]Sandrine Blazy, Philippe Facon:
Partial Evaluation for the Understanding of Fortran Programs. Int. J. Softw. Eng. Knowl. Eng. 4(4): 535-559 (1994) - [c5]Sandrine Blazy, Philippe Facon:
SFAC, a tool for program comprehension by specialization. WPC 1994: 162-167 - 1993
- [c4]Sandrine Blazy, Philippe Facon:
Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs. CAiSE 1993: 184-198 - [c3]Sandrine Blazy, Philippe Facon:
Partial evaluation as an aid to the comprehension of Fortran programs. WPC 1993: 46-54 - [c2]Sandrine Blazy, Philippe Facon:
Partial Evaluation for the Understanding of FORTRAN Programs. SEKE 1993: 517-525 - 1992
- [c1]Marc Haziza, J. F. Voidrot, E. Minor, L. Pofelski, Sandrine Blazy:
Software maintenance: an analysis of industrial needs and constraints. ICSM 1992: 18-26
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-05 21:10 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
