Circuits as streams in Coq: Verification of a sequential multiplier

DOI10.1007/3-540-61780-9_72zbMath1407.68439OpenAlexW1536384265MaRDI QIDQ4647582

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

higher-order logichardware verificationsequential circuitsequential multipliermultiplier circuit

Mathematics Subject Classification ID

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

Related Items (3)

The simplicial model of univalent foundations (after Voevodsky) ⋮ Using a generalisation critic to find bisimulations for coinductive proofs ⋮ Functional verification of high performance adders in \textsc{Coq}

Uses Software

• Coq
• ML
• HOL
• NQTHM

Cites Work

• Certifying circuits in type theory
• A note on categorical datatypes
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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