BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × Cyprus
1 × France
1 × Germany
1 × India
1 × Ireland
1 × Spain
2 × USA
Collaborated with:
P.Facon B.Robillard V.Laporte D.Pichardie X.Leroy S.Riaud T.Sirvent J.Kriener A.King A.W.Appel Z.Dargaye A.Maroneze J.Jourdan F.Besson A.Dang T.P.Jensen P.Wilke G.Barthe B.Grégoire Rémi Hutin Alix Trieu
Talks about:
formal (8) program (4) verif (4) compil (3) understand (2) special (2) softwar (2) partial (2) fortran (2) coalesc (2)

Person: Sandrine Blazy

DBLP DBLP: Blazy:Sandrine

Facilitated 1 volumes:

SAS 2015Ed

Contributed to:

POPL 20152015
SCAM 20152015
PPDP 20132013
SAS 20132013
ESOP 20102010
LCTES 20092009
FM 20062006
ASE 19971997
WPC 19961996
CAiSE 19931993
SEKE 19931993
ESOP 20192019
POPL 20202020

Wrote 14 papers:

POPL-2015-JourdanLBLP #c
A Formally-Verified C Static Analyzer (JHJ, VL, SB, XL, DP), pp. 247–259.
SCAM-2015-BlazyRS #obfuscation
Data tainting and obfuscation: Improving plausibility of incorrect taint (SB, SR, TS), pp. 111–120.
PPDP-2013-KrienerKB #coq #prolog #proving #semantics
Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.
SAS-2013-BlazyLMP #abstract interpretation #analysis #c #verification
Formal Verification of a C Value Analysis Based on Abstract Interpretation (SB, VL, AM, DP), pp. 324–344.
ESOP-2010-BlazyRA #graph #verification
Formal Verification of Coalescing Graph-Coloring Register Allocation (SB, BR, AWA), pp. 145–164.
LCTES-2009-BlazyR #performance
Live-range unsplitting for faster optimal coalescing (SB, BR), pp. 70–79.
FM-2006-BlazyDL #c #compilation #verification
Formal Verification of a C Compiler Front-End (SB, ZD, XL), pp. 460–475.
ASE-1997-BlazyF #development #formal method #maintenance
Application of Formal Methods to the Development of a Software Maintenance Tool (SB, PF), pp. 162–171.
WPC-1996-BlazyF #analysis #comprehension #interprocedural
Interprocedural analysis for program comprehension by specialization (SB, PF), p. 133–?.
CAiSE-1993-BlazyF #comprehension #fortran #partial evaluation #source code #symbolic computation
Partial Evaluation and Symbolic Computation for the Understanding of Fortran Programs (SB, PF), pp. 184–198.
SEKE-1993-BlazyF #comprehension #fortran #partial evaluation #source code
Partial Evaluation for the Understanding of FORTRAN Programs (SB, PF), pp. 517–525.
TAPSOFT-1995-BlazyF #prototype #specification
Formal Specification and Prototyping of a Program Specializer (SB, PF), pp. 666–680.
ESOP-2019-BessonBDJW #compilation #fault
Compiling Sandboxes: Formally Verified Software Fault Isolation (FB, SB, AD, TPJ, PW), pp. 499–524.
POPL-2020-BartheBGHLPT #c #compilation #verification
Formal verification of a constant-time preserving C compiler (GB, SB, BG, RH, VL, DP, AT), p. 30.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.