Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)

DOI10.1007/978-3-319-94821-8_21OpenAlexW2810387547MaRDI QIDQ1791178

Zachary Tatlock, Ramana Kumar, Eric Mullen, Magnus O. Myreen

Publication date: 4 October 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-94821-8_21

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

\texttt{cake\_lpr}: verified propagation redundancy checking in CakeML

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• CakeML
• CompCert
• Fiat
• CertiCoq
• OEuf

This page was built for publication: Software verification with ITPs should use binary code extraction to reduce the TCB (short paper)