Sandrine Blazy
17
Documents
Identifiants chercheurs
sandrine-blazy-
0000-0002-0189-0223
- IdRef : 153042567
Présentation
Publications
- 3
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 17
- 7
- 4
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 2
- 2
- 1
- 2
- 2
- 3
- 2
- 3
- 5
- 1
- 1
|
|
Formally verified speculation and deoptimization in a JIT compilerProceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.26. ⟨10.1145/3434327⟩
Article dans une revue
hal-03185848v1
|
|
|
Formal verification of a constant-time preserving C compilerProceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-30. ⟨10.1145/3371075⟩
Article dans une revue
hal-02975012v1
|
|
|
Verifying constant-time implementations by abstract interpretationJournal of Computer Security, 2019, 27 (1), pp.137--163. ⟨10.3233/JCS-181136⟩
Article dans une revue
hal-02025047v1
|
|
|
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying CodeJournal of Automated Reasoning, 2016, 56 (3), pp.26. ⟨10.1007/s10817-015-9359-8⟩
Article dans une revue
hal-01243700v1
|
|
|
Secure Compilation of Constant-Resource ProgramsCSF 2021 - 34th IEEE Computer Security Foundations Symposium, Jun 2021, Dubrovnik, Croatia. pp.1-12
Communication dans un congrès
hal-03221440v1
|
|
|
A Fast Verified Liveness Analysis in SSA FormIJCAR 2020- International Joint Conference on Automated Reasoning, Jun 2020, Paris, France. pp.324-340, ⟨10.1007/978-3-030-51054-1_19⟩
Communication dans un congrès
hal-02904204v1
|
|
|
Verified Translation Validation of Static AnalysesComputer Security Foundations Symposium, Aug 2017, Santa-Barbara, United States
Communication dans un congrès
hal-01588422v1
|
|
|
Verifying Constant-Time Implementations by Abstract InterpretationEuropean Symposium on Research in Computer Security, Sep 2017, Oslo, Norway
Communication dans un congrès
hal-01588444v1
|
|
|
An Abstract Memory Functor for Verified C Static AnalyzersACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. pp.14, ⟨10.1145/2951913.2951937⟩
Communication dans un congrès
hal-01339969v1
|
Verified Validation of Program SlicingCPP 2015 : Conference on Certified Programs and Proofs, 2015, Mumbai, India. pp.109-117, ⟨10.1145/2676724.2693169⟩
Communication dans un congrès
hal-01110821v1
|
|
|
|
A formally-verified C static analyzerPOPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩
Communication dans un congrès
hal-01078386v1
|
|
|
Validating Dominator Trees for a Fast, Verified Dominance TestInteractive Theorem Proving, Aug 2015, Nanjing, China. ⟨10.1007/978-3-319-22102-1_6⟩
Communication dans un congrès
hal-01193281v1
|
A Formally Verified WCET Estimation Tool14th International Workshop on Worst-Case Execution Time Analysis, Jul 2014, Madrid, Spain. ⟨10.4230/OASIcs.WCET.2014.11⟩
Communication dans un congrès
hal-01087194v1
|
|
|
|
Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying CodeThe 5th International Conference on Interactive Theorem Proving (ITP 2014), 2014, Vienna, Austria. pp.128 - 143, ⟨10.1007/978-3-319-08970-6_9⟩
Communication dans un congrès
hal-01102445v1
|
|
|
Formal Verification of Loop Bound Estimation for WCET AnalysisVSTTE - Verified Software: Theories, Tools and Experiments, Natarajan Shankar, May 2013, Menlo Park, United States. pp.281-303
Communication dans un congrès
hal-00848703v1
|
|
|
Formal Verification of a C Value Analysis Based on Abstract InterpretationSAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. pp.324-344
Communication dans un congrès
hal-00812515v1
|
Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. ProceedingsBlazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David. Springer, 7998, pp.500, 2013, Lecture Notes in Computer Science, ⟨10.1007/978-3-642-39634-2⟩
Ouvrages
hal-00908865v1
|