Verified abstract interpretation techniques for disassembling low-level self-modifying code

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

zbMATH Keywords

abstract interpretationCoqlow-level programming language

Mathematics Subject Classification ID

Related Items (2)

LTL model checking of self modifying code ⋮ Reachability Analysis of Self Modifying Code

Uses Software

• Coq
• VeriStar
• Rocksalt

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