×
Edit Profile (opens in new tab)

Blazy, Sandrine

Co-Author Distance
Author ID: blazy.sandrine Recent zbMATH articles by "Blazy, Sandrine"
Published as: Blazy, Sandrine
Documents Indexed: 19 Publications since 1996, including 1 Book
4 Contributions as Editor
Co-Authors: 20 Co-Authors with 20 Joint Publications
195 Co-Co-Authors
all top 5

Co-Authors

1 single-authored
7 Pichardie, David
5 Besson, Frédéric
5 Wilke, Pierre
3 Appel, Andrew W.
3 Laporte, Vincent
3 Leroy, Xavier
2 Chechik, Marsha
1 Beringer, Lennart
1 Borchers, Wolfgang
1 Dang, Alexandre
1 Demange, Delphine
1 Dockins, Robert
1 Dodds, Josiah
1 Dralle, U.
1 Gervais, Frédéric
1 Hobor, Aquinas
1 Laleau, Régine
1 Léchenet, Jean-Christophe
1 Paulin-Mohring, Christine
1 Robillard, Benoît
1 Stewart, Gordon
1 Trieu, Alix

Serials

6 Journal of Automated Reasoning
3 Lecture Notes in Computer Science

Fields

22 Computer science (68-XX)
3 General and overarching topics; collections (00-XX)
1 Numerical analysis (65-XX)
1 Fluid mechanics (76-XX)

Publications by Year

all cited Publications top 5 cited Publications

Citations contained in zbMATH Open

13 Publications have been cited 128 times in 108 Documents Cited by ▼ Year ▼
Program logics for certified compilers. Zbl 1298.68009
Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier
31
2014
Mechanized semantics for the clight subset of the C language. Zbl 1185.68136
Blazy, Sandrine; Leroy, Xavier
27
2009
Formal verification of a C-like memory model and its uses for verifying program transformations. Zbl 1154.68039
Leroy, Xavier; Blazy, Sandrine
23
2008
Separation logic for small-step Cminor. Zbl 1144.68351
Appel, Andrew W.; Blazy, Sandrine
19
2007
Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Zbl 1268.68006
8
2013
Formal verification of coalescing graph-coloring register allocation. Zbl 1260.68227
Blazy, Sandrine; Robillard, Benoît; Appel, Andrew W.
5
2010
Verifying constant-time implementations by abstract interpretation. Zbl 1496.68100
Blazy, Sandrine; Pichardie, David; Trieu, Alix
3
2017
A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. Zbl 1465.68041
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
3
2019
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
A concrete memory model for CompCert. Zbl 1465.68040
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
2
2015
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
2
2015
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1357.68041
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1417.68030
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
1
2014
A verified CompCert front-end for a memory model supporting pointer arithmetic and uninitialised data. Zbl 1465.68041
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
3
2019
Verifying constant-time implementations by abstract interpretation. Zbl 1496.68100
Blazy, Sandrine; Pichardie, David; Trieu, Alix
3
2017
An abstract memory functor for verified C static analyzers. Zbl 1361.68058
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1357.68041
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
2
2016
A concrete memory model for CompCert. Zbl 1465.68040
Besson, Frédéric; Blazy, Sandrine; Wilke, Pierre
2
2015
Validating dominator trees for a fast, verified dominance test. Zbl 1466.68030
Blazy, Sandrine; Demange, Delphine; Pichardie, David
2
2015
Program logics for certified compilers. Zbl 1298.68009
Appel, Andrew W.; Dockins, Robert; Hobor, Aquinas; Beringer, Lennart; Dodds, Josiah; Stewart, Gordon; Blazy, Sandrine; Leroy, Xavier
31
2014
Verified abstract interpretation techniques for disassembling low-level self-modifying code. Zbl 1417.68030
Blazy, Sandrine; Laporte, Vincent; Pichardie, David
1
2014
Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Zbl 1268.68006
8
2013
Formal verification of coalescing graph-coloring register allocation. Zbl 1260.68227
Blazy, Sandrine; Robillard, Benoît; Appel, Andrew W.
5
2010
Mechanized semantics for the clight subset of the C language. Zbl 1185.68136
Blazy, Sandrine; Leroy, Xavier
27
2009
Formal verification of a C-like memory model and its uses for verifying program transformations. Zbl 1154.68039
Leroy, Xavier; Blazy, Sandrine
23
2008
Separation logic for small-step Cminor. Zbl 1144.68351
Appel, Andrew W.; Blazy, Sandrine
19
2007
all cited Publications top 5 cited Publications
all top 5

Cited by 225 Authors

11 Appel, Andrew W.
9 Blazy, Sandrine
8 Krebbers, Robbert
7 Leroy, Xavier
5 Beringer, Lennart
5 Birkedal, Lars
5 Pichardie, David
4 Besson, Frédéric
4 Wilke, Pierre
3 Barthe, Gilles
3 Bengtson, Jesper
3 Bizjak, Aleš
3 Cruz-Filipe, Luís
3 Dreyer, Derek R.
3 Hobor, Aquinas
3 Kosmatov, Nikolai
3 Schneider-Kamp, Peter
3 Vafeiadis, Viktor
2 Abate, Carmine
2 Cao, Qinxiang
2 Crespo, Juan Manuel
2 Cuellar, Santiago
2 Dockins, Robert
2 Ene, Cristian
2 Gallagher, John P.
2 Gu, Ronghui
2 Hack, Sebastian
2 Hermenegildo, Manuel V.
2 Hriţcu, Cătălin
2 Jourdan, Jacques-Henri
2 Jung, Ralf
2 Kumar, Ramana
2 Kunz, César
2 Lammich, Peter
2 Laporte, Vincent
2 Larsen, Kim Skak
2 Le Gall, Pascale
2 Léchenet, Jean-Christophe
2 McCreight, Andrew
2 Meseguer Guaita, José
2 Mounier, Laurent
2 Myreen, Magnus O.
2 Norrish, Michael
2 Owens, Scott
2 Pagel, Jens
2 Potet, Marie-Laure
2 Ramananandro, Tahina
2 Roşu, Grigore
2 Schneider, Sigurd
2 Sewell, Peter
2 Shao, Zhong
2 Smolka, Gert
2 Tan, Yong Kiam
2 Tolmach, Andrew
2 Touili, Tayssir
2 Wu, Xiongnan
2 Ye, Xin
2 Zappa Nardelli, Francesco
2 Zuleger, Florian
1 Abrahamsson, Oskar
1 Anureev, Igor’ Sergeevich
1 Asăvoae, Irina Măriuca
1 Asăvoae, Mihail
1 Azevedo de Amorim, Arthur
1 Bacelar Almeida, José
1 Bannister, Callum
1 Barbosa, Manuel
1 Benton, Nick
1 Berdine, Josh
1 Bereczky, Péter
1 Betarte, Gustavo
1 Blanco, Roberto
1 Blatter, Lionel
1 Bodin, Martin
1 Boender, Jaap P.
1 Bowen, Jonathan P.
1 Busi, Matteo
1 Campo, Juan Diego
1 Casinghino, Chris
1 Charguéraud, Arthur
1 Chen, Hao
1 Chevalier, Tim
1 Ciobâcă, Ştefan
1 Cohen, Cyril
1 Cohen, Joshua M.
1 Collins, Nathan A.
1 Courant, Nathanaël
1 De Angelis, Emanuele
1 DeHon, Andre
1 Demange, Delphine
1 Doczkal, Christian
1 Dodds, Josiah
1 Dos Reis, Gabriel
1 Duan, Zhenhua
1 Durier, Adrien
1 Filaretti, Daniele
1 Fioravanti, Fabio
1 Fisher, Kathleen
1 Fox, Anthony C. J.
1 Fridlender, Daniel
...and 125 more Authors
all top 5

Cited in 13 Serials

18 Journal of Automated Reasoning
3 Journal of Functional Programming
2 Theoretical Computer Science
2 Formal Methods in System Design
2 Logical Methods in Computer Science
2 Journal of Logical and Algebraic Methods in Programming
1 Information and Computation
1 Formal Aspects of Computing
1 Mathematical Structures in Computer Science
1 International Journal of Foundations of Computer Science
1 Theory and Practice of Logic Programming
1 ACM Transactions on Computational Logic
1 Modelirovanie i Analiz Informatsionnykh Sistem
all top 5

Cited in 8 Fields

105 Computer science (68-XX)
30 Mathematical logic and foundations (03-XX)
3 Information and communication theory, circuits (94-XX)
1 Ordinary differential equations (34-XX)
1 Probability theory and stochastic processes (60-XX)
1 Quantum theory (81-XX)
1 Operations research, mathematical programming (90-XX)
1 Systems theory; control (93-XX)

Citations by Year