Coq and hardware verification: a case study

DOI10.1007/BFB0105401MaRDI QIDQ6567708zbMATH OpenFDO

Authors Solange Coupet-Grimal, Line Jakubiec

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105401

Mathematics Subject Classification ID

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

Recommendations

• Coquet: a Coq library for verifying hardware
• Certifying circuits in type theory
• Circuits as streams in Coq: verification of a sequential multiplier
• Using an induction prover for verifying arithmetic circuits
• scientific article; zbMATH DE number 1070623

Cites work

• scientific article; zbMATH DE number 3928956 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• CtCoq: a system presentation
• Edinburgh LCF. A mechanized logic of computation
• The system \({\mathcal F}\) of variable types, fifteen years later

This page was built for publication: Coq and hardware verification: a case study

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6567708)