A Formally-Verified Alias Analysis
From MaRDI portal
Publication:4916050
DOI10.1007/978-3-642-35308-6_5zbMath1383.68015OpenAlexW61954547MaRDI QIDQ4916050
Publication date: 19 April 2013
Published in: Certified Programs and Proofs (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00773109/file/alias-analysis.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
A generic framework for heap and value analyses of object-oriented programming languages ⋮ Verified abstract interpretation techniques for disassembling low-level self-modifying code ⋮ Expression-Based Aliasing for OO–languages ⋮ Aliasing Restrictions of C11 Formalized in Coq ⋮ CompCertS: a memory-aware verified C compiler using pointer as integer semantics ⋮ A formal C memory model for separation logic ⋮ System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory ⋮ \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
Uses Software
This page was built for publication: A Formally-Verified Alias Analysis
