An abstract memory functor for verified C static analyzers
From MaRDI portal
Publication:2985780
DOI10.1145/2951913.2951937zbMath1361.68058MaRDI QIDQ2985780
David Pichardie, Sandrine Blazy, Vincent Laporte
Publication date: 10 May 2017
Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01339969/file/main.pdf
numerical analysis; abstract interpretation; Coq proof assistant; points-to analysis; low-level memory
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Certified compilation for cryptography: extended x86 instructions and constant-time verification, Verifying constant-time implementations by abstract interpretation
Uses Software