Sandrine Blazy
Former news
- [11/2020] Invited talk: From Verified Compilation to Secure Compilation: a Semantic Approach,
ACM SIGSAC PLAS 2020 workshop
- [09/2019] Invited talk: Formal Verification of a Constant-Time Preserving C Compiler,
Verified software workshop,
Newton institute, Cambridge, United Kingdom
- [05/2019] Effective
Verification: Static Analysis Meets Program Logics, Lorentz center, Netherlands
- [12/2018] Invited talk: Semantics
preservation of program obfuscations, GDR Sécurité, Paris Saclay
- [07/2016] Logic and Semantics Seminar, Cambridge, United Kingdom
- [08/2015] Coq tutorial, ITP conference,
Nanjing, China
- [04/2015] Dagstuhl seminar: Qualification
of formal methods tools, Germany
- [03/2015] NII Shonan meeting on low-level code analysis and applications to computer security, Japan
- [01/2015] Programming
Languages Mentoring Workshop, PLMW 2015, India
- [08/2014] NII Shonan summer school on Coq, Japan
- [06/2014] Dagstuhl seminar: Challenges in
Analysing Executables: Scalability, Self-Modifying Code and Synergy
- [01/2014] Invited talk (in French): Formal
verification of a graph coloring algorithm for register
allocation, JFLA 2014 (session in honor of JFLA's 25th birthday), previously published in JFLA 2008
- [05/2013] A tutorial on the CompCert verified
compiler, invited talk, VSTTE 2013 conference, Menlo Park, USA
Former program committees
-
FMTea 2021,
AFADL 2021,
Types 2021,
GPCE 2020,
AFADL 2020,
TyDe 2020,
- ICFP 2020 (ERC),
POPL 2020,
PriSC 2020,
APLAS 2019,
SpISA 2019,
ITP 2019,
AFADL 2019,
- LOPSTR 2018,
ICFP 2018,
AFADL 2018,
EuroS&P 2018,
CPP 2018,
IFL 2017,
- SRC@PLDI 2017,
TFP 2017,
GPCE 2017,
VSTTE 2017,
AFADL 2017,
CoqPL 2017 (co-chair),
-
PLMW@SPLASH 2016 (co-chair),
APLAS 2016,
IFL 2016,
-
VSTTE 2016 (co-chair),
GPCE'16,
DS@STAF16,
AFADL 2016,
CPP
2016,
- SAS 2015
(co-chair),
OCaml workshop 2015,
ITP 2015,
AFADL 2015,
-
VSTTE 2014,
AFADL 2014,
CC
2014,
LPAR 2013,
ITP 2013 (co-chair),
VMCAI
2013, ITP 2011
Former research projects
- ERC VESTA:
verified static analysis platform (2018-2021) led by David Pichardie
- Scrypt
(funded by grant ANR-18-CE25-0014):
secure compilation for cryptography (2019-2022)
- AnaStaSec
(funded by grant ANR-14-CE28-0014):
static analysis for security properties (2015-2017)
- BINSEC
(funded by grant ANR-12-INSE-002):
binary code analysis for security (2013-2016)
- VERASCO
(funded by grant ANR-11-INSE-003):
formal verification of static analyzers and of compilers
(2012-2015)
- ASCERT
(funded by FNRAE):
formal verification of static analysis (2009-2012)
- U3CAT (funded
by ANR-08-SEGI-021):
unification of critical C code analysis techniques
inside the Frama-C
platform (2008-2011).
- CompCert
(funded by ANR):
formal verification of a C compiler (2005-2007)