Modular development of certified program verifiers with a proof assistant,

DOI10.1017/S0956796808006904zbMath1155.68429MaRDI QIDQ3546045

Adam Chlipala

Publication date: 18 December 2008

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Extensible and Efficient Automation Through Reflective Tactics

Uses Software

• Coq

Cites Work

• Proof-carrying code from certified abstract interpretation and fixpoint compression
• A syntactic approach to foundational proof-carrying code
• Extracting a data flow analyser in constructive logic
• Verified lightweight bytecode verification
• Stack-based typed assembly language
• The view from the left

This page was built for publication: Modular development of certified program verifiers with a proof assistant,