Circuits as streams in Coq: verification of a sequential multiplier

DOI10.1007/3-540-61780-9_72zbMATH Open1407.68439OpenAlexW1536384265MaRDI QIDQ4647582FDOQ4647582

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

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

zbMATH Keywords

hardware verificationhigher-order logicsequential circuitsequential multipliermultiplier circuit

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A note on categorical datatypes
• Title not available (Why is that?)
• 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

Uses Software

• Coq
• ML
• HOL
• NQTHM

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)