A Formalization of the C99 Standard in HOL, Isabelle and Coq

DOI10.1007/978-3-642-22673-1_28zbMath1335.68233OpenAlexW2005097112MaRDI QIDQ5200133

Robbert Krebbers, Freek Wiedijk

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22673-1_28

Mathematics Subject Classification ID

Related Items (2)

Aliasing Restrictions of C11 Formalized in Coq ⋮ A formal C memory model for separation logic

Uses Software

• Coq
• Isabelle
• Ott
• Isabelle/HOL
• HOL
• VCC

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Mechanized semantics for the clight subset of the C language
• Ott: Effective tool support for the working semanticist

This page was built for publication: A Formalization of the C99 Standard in HOL, Isabelle and Coq