Abstract interpretation-based certification of assembly code
From MaRDI portal
Recommendations
- Certified Static Analysis by Abstract Interpretation
- Symbolic transfer function-based approaches to certified compilation
- Analyzing Information Flow Properties in Assembly Code by Abstract Interpretation
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Certifying assembly programs with trails
Cited in
(13)- Fully abstract trace semantics for protected module architectures
- Certified abstract cost analysis
- Verified abstract interpretation techniques for disassembling low-level self-modifying code
- Verified abstract interpretation techniques for disassembling low-level self-modifying code
- Hardware-Dependent Proofs of Numerical Programs
- Symbolic transfer function-based approaches to certified compilation
- Certifying assembly programs with trails
- scientific article; zbMATH DE number 1019594 (Why is no real title available?)
- Pretty-big-step-semantics-based certified abstract interpretation (preliminary version)
- Highly automated formal proofs over memory usage of assembly code
- Certificate Translation in Abstract Interpretation
- Relational abstract interpretation of arrays in assembly code
- Translation and run-time validation of loop transformations
This page was built for publication: Abstract interpretation-based certification of assembly code
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4414379)
