Circuits as streams in Coq: verification of a sequential multiplier

DOI10.1007/3-540-61780-9_72MaRDI QIDQ4647582zbMATH OpenOpenAlexFDO

Authors Christine Paulin-Mohring

Publication date 15 January 2019

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

Full work available at URL https://hal-lara.archives-ouvertes.fr/hal-02101845/file/RR1995-16.pdf

zbMATH Keywords

hardware verificationhigher-order logicsequential circuitsequential multipliermultiplier circuit

Mathematics Subject Classification ID

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

Recommendations

• Certifying circuits in type theory
• Coquet: a Coq library for verifying hardware
• CIRC: A Circular Coinductive Prover
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Using an induction prover for verifying arithmetic circuits

Cites work

• scientific article; zbMATH DE number 3991418 (Why is no real title available?)
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A note on categorical datatypes
• Certifying circuits in type theory

Cited in

(6)

• Coquet: a Coq library for verifying hardware
• Coq and hardware verification: a case study
• Functional verification of high performance adders in \textsc{Coq}
• The simplicial model of univalent foundations (after Voevodsky)
• Certifying circuits in type theory
• Using a generalisation critic to find bisimulations for coinductive proofs

Describes a project that uses

Uses Software

• NQTHM
• HOL
• ML
• Coq

This page was built for publication: Circuits as streams in Coq: verification of a sequential multiplier

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