New developments in the theory of Gröbner bases and applications to formal verification

DOI10.1016/j.jpaa.2008.11.043zbMath1164.68019arXiv0801.1177OpenAlexW2137378957MaRDI QIDQ1017680

Gert-Martin Greuel, Oliver Wienand, Markus Wedler, Alexander Dreyer, Michael Brickenstein

Publication date: 12 May 2009

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0801.1177

zbMATH Keywords

Boolean functionspolynomial ringBoolean Gröbner basesformal verification of digital circuitsstandard bases over rings

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Polynomial rings and ideals; rings of integer-valued polynomials (13F20) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Specification and verification (program logics, model checking, etc.) (68Q60) Boolean functions (06E30)

Related Items

Narrow Proofs May Be Maximally Long, Role of involutive criteria in computing Boolean Gröbner bases, Minimal Gröbner bases and the predictable leading monomial property, Space Complexity in Polynomial Calculus, Cohomology, Bocksteins, and resonance varieties in characteristic 2, Obtaining and solving systems of equations in key variables only for the small variants of AES, An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths, Boolean Gröbner bases, On computation of Boolean involutive bases, BIBasis, a package for REDUCE and Macaulay2 computer algebra systems to compute Boolean involutive and Gröbner bases, Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases, Polybori: A framework for Gröbner-basis computations with Boolean polynomials, Boolean ideals and their varieties

Uses Software

• CoCoA
• Macaulay2
• MiniSat
• PolyBoRi
• SageMath
• SINGULAR
• slimgb
• SATLIB
• CUDD
• Python

Cites Work

• Algorithmic properties of polynomial rings
• Converting bases with the Gröbner walk
• Unique Factorization Rings with Zero Divisors
• Unique factorization rings with zero divisors
• Theory and Applications of Satisfiability Testing
• Interpolants and Symbolic Model Checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item