Coq and hardware verification: a case study

DOI10.1007/BFB0105401zbMATH Open1543.682MaRDI QIDQ6567708FDOQ6567708

Authors: Solange Coupet-Grimal, Line Jakubiec 

Publication date: 5 July 2024

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

Mathematics Subject Classification ID

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

Cites Work

• Edinburgh LCF. A mechanized logic of computation
• The system \({\mathcal F}\) of variable types, fifteen years later
• Title not available (Why is that?)
• Title not available (Why is that?)
• CtCoq: a system presentation

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)