Functional verification of high performance adders in \textsc{Coq}

DOI10.1155/2014/197252zbMath1437.68191OpenAlexW2029501708WikidataQ59050211 ScholiaQ59050211MaRDI QIDQ2336214

Yanyan Li

Publication date: 19 November 2019

Published in: Journal of Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1155/2014/197252

Mathematics Subject Classification ID

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

Uses Software

• Coq
• PREVAIL
• Coquet
• CoqMTU

Cites Work

• Unnamed Item
• Unnamed Item
• Formal proof of prefix adders
• Hardware specification, verification and synthesis: mathematical aspects. Mathematical Sciences Institute workshop, Ithaca, NY, USA, July 5--7, 1989. Proceedings
• Certifying circuits in type theory
• Coquet: A Coq Library for Verifying Hardware
• Circuits as streams in Coq: Verification of a sequential multiplier
• FUNCTIONAL PEARL Derivation of a logarithmic time carry lookahead addition circuit
• Mathematics of Program Construction
• A Parallel Algorithm for the Efficient Solution of a General Class of Recurrence Equations

This page was built for publication: Functional verification of high performance adders in \textsc{Coq}