Verified abstract interpretation techniques for disassembling low-level self-modifying code
From MaRDI portal
Publication:287369
DOI10.1007/s10817-015-9359-8zbMath1357.68041OpenAlexW2293328630MaRDI QIDQ287369
Vincent Laporte, Sandrine Blazy, David Pichardie
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01243700/file/main.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Uses Software
Cites Work
- Extracting a data flow analyser in constructive logic
- Mechanized semantics for the clight subset of the C language
- Abstract Interpretation of Annotated Commands
- High-level separation logic for low-level code
- Refinement-Based CFG Reconstruction from Unstructured Programs
- Grammar Analysis and Parsing by Abstract Interpretation
- A Formally-Verified Alias Analysis
- Verified heap theorem prover by paramodulation
- Structural Abstract Interpretation: A Formal Study Using Coq
- Verified just-in-time compiler on x86
- Building Certified Static Analysers by Modular Construction of Well-founded Lattices
- A Certified Denotational Abstract Interpreter
- Types for Proofs and Programs
- Types for Proofs and Programs
This page was built for publication: Verified abstract interpretation techniques for disassembling low-level self-modifying code