An abstract memory functor for verified C static analyzers

DOI10.1145/2951913.2951937zbMath1361.68058OpenAlexW2515025958MaRDI 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

zbMATH Keywords

numerical analysisabstract interpretationCoq proof assistantpoints-to analysislow-level memory

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Certified compilation for cryptography: extended x86 instructions and constant-time verification ⋮ Verifying constant-time implementations by abstract interpretation

Uses Software

• Coq
• ASTREE
• Verasco

This page was built for publication: An abstract memory functor for verified C static analyzers