Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry

DOI10.1007/S10703-014-0206-ZMaRDI QIDQ479832zbMATH OpenOpenAlexFDO

Authors Alexey Lvov, Luis A. Lastras-Montaño, Viresh Paruthi, Robert Shadowen, Ali El-Zein, Barry Trager

Publication date 5 December 2014

Published in Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10703-014-0206-z

zbMATH Keywords

Buchberger algorithmerror correcting circuitsformal verificationGalois finite fields

Mathematics Subject Classification ID

Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Decoding (94B35) Analytic circuit theory (94C05)

Recommendations

• Formal Approach for Verifying Galois Field Arithmetic Circuits of Higher Degrees
• scientific article; zbMATH DE number 1796154
• Formal Verification of Integer Multiplier Circuits Using Algebraic Reasoning: A Survey
• A formal verification method of error correction code processors over Galois-field arithmetic
• Artificial Intelligence and Symbolic Computation
• scientific article; zbMATH DE number 524110
• On validated computing in algebraic number fields
• Formal verification of n-bit ALU using theorem proving
• Incremental column-wise verification of arithmetic circuits using computer algebra

Cites work

• Formal Methods in Computer-Aided Design
• Graph-Based Algorithms for Boolean Function Manipulation
• scientific article; zbMATH DE number 107542 (Why is no real title available?)
• scientific article; zbMATH DE number 1796154 (Why is no real title available?)

Cited in

(5)

• An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
• scientific article; zbMATH DE number 1796154 (Why is no real title available?)
• A formal verification method of error correction code processors over Galois-field arithmetic
• Verification, Model Checking, and Abstract Interpretation
• Verified Erasure Correction in Coq with MathComp and VST

Describes a project that uses

Uses Software

• SINGULAR
• STABLE
• BLUEVERI

This page was built for publication: Verification of Galois field based circuits by formal reasoning based on computational algebraic geometry

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