An abstract memory functor for verified C static analyzers
From MaRDI portal
Recommendations
- A certified denotational abstract interpreter
- Verified functional programming of an abstract interpreter
- A concrete memory model for CompCert
- \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
Cited in
(12)- Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
- Verified functional programming of an abstract interpreter
- Certified compilation for cryptography: extended x86 instructions and constant-time verification
- Verifying constant-time implementations by abstract interpretation
- \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
- Hierarchical shape abstraction for analysis of free list memory allocators
- Access analysis-based tight localization of abstract memories
- Statically inferring complex heap, array, and numeric invariants
- Inferring effective types for static analysis of C programs
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Computer Algebra in Scientific Computing
- A certified denotational abstract interpreter
This page was built for publication: An abstract memory functor for verified C static analyzers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2985780)
