Formal verification of n-bit ALU using theorem proving

DOI10.1007/978-3-030-03044-5_6MaRDI QIDQ6165885zbMATH OpenOpenAlexFDO

Authors

Publication date 2 August 2023

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

Full work available at URL https://doi.org/10.1007/978-3-030-03044-5_6

Mathematics Subject Classification ID

Networks and circuits as models of computation; circuit complexity (68Q06) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20) Switching theory, applications of Boolean algebras to circuits and networks (94C11)

Recommendations

• scientific article; zbMATH DE number 139822
• Formal reliability analysis of combinational circuits using theorem proving
• scientific article; zbMATH DE number 1670746
• Formalization of linear space theory in the higher-order logic proving system
• scientific article; zbMATH DE number 1088222

Cited in

(3)

• Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry
• Polynomial Formal Verification of Approximate Functions
• Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2

This page was built for publication: Formal verification of n-bit ALU using theorem proving

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