Sandrine Blazy
6
Documents
Identifiants chercheurs
- sandrine-blazy
- 0000-0002-0189-0223
- IdRef : 153042567
Présentation
Publications
- 2
- 2
- 2
- 2
- 6
- 6
- 1
- 1
- 3
- 1
- 1
- 1
- 1
- 1
|
A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised DataJournal of Automated Reasoning, 2019, 62 (4), pp.433-480. ⟨10.1007/s10817-017-9439-z⟩
Article dans une revue
hal-01656895v1
|
|
CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer SemanticsJournal of Automated Reasoning, 2019, 63 (2), pp.369-392. ⟨10.1007/s10817-018-9496-y⟩
Article dans une revue
hal-02401182v1
|
|
Compiling Sandboxes: Formally Verified Software Fault IsolationESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. pp.499-524, ⟨10.1007/978-3-030-17184-1_18⟩
Communication dans un congrès
hal-02316189v1
|
|
CompCertS: A Memory-Aware Verified C Compiler using Pointer as Integer SemanticsITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.81-97, ⟨10.1007/978-3-319-66107-0_6⟩
Communication dans un congrès
hal-01656875v1
|
|
A Concrete Memory Model for CompCertITP 2015 : 6th International Conference on Interactive Theorem Proving, Aug 2015, Nanjing, China. pp.67-83, ⟨10.1007/978-3-319-22102-1_5⟩
Communication dans un congrès
hal-01194549v1
|
|
A Precise and Abstract Memory Model for C Using Symbolic Values12th Asian Symposium on Programming Languages and Systems (APLAS 2014), 2014, Singapore, Singapore. pp.449 - 468, ⟨10.1007/978-3-319-12736-1_24⟩
Communication dans un congrès
hal-01093312v1
|