Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2

DOI10.4204/EPTCS.359.11MaRDI QIDQ6659923zbMATH OpenFDO

Authors Mertcan Temel

Publication date 9 January 2025

Full work available at URL https://doi.org/10.4204/EPTCS.359.11

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Automated and scalable verification of integer multipliers
• scientific article; zbMATH DE number 1507199
• Formal Verification of Structurally Complex Multipliers
• Formal verification of n-bit ALU using theorem proving
• scientific article; zbMATH DE number 1670746

Cited in

(1)

• Using ACL2 in the design of efficient, verifiable data structures for high-assurance systems

This page was built for publication: Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2

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