A formally-verified alias analysis

DOI10.1007/978-3-642-35308-6_5MaRDI QIDQ4916050zbMATH OpenOpenAlexFDO

Authors Valentin Robert, Xavier Leroy

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

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Recommendations

• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• CompCertS: a memory-aware verified C compiler using pointer as integer semantics
• Certified Static Analysis by Abstract Interpretation
• Types for Proofs and Programs
• A formally verified compiler back-end

Cited in

(17)

• ALIAS: a modular tool for finding backdoors for SAT
• 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
• scientific article; zbMATH DE number 1693485 (Why is no real title available?)
• A generic framework for heap and value analyses of object-oriented programming languages
• Verified abstract interpretation techniques for disassembling low-level self-modifying code
• A logical analysis of aliasing in imperative higher-order functions
• Aliasing restrictions of C11 formalized in Coq
• Expression-Based Aliasing for OO–languages
• Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors
• A logical analysis of aliasing in imperative higher-order functions
• Compiler Construction
• Evaluating the effectiveness of pointer alias analyses
• Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
• Transformational derivation of an improved alias analysis algorithm

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A formally-verified alias analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4916050)