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

DOI10.1016/J.JPAA.2008.11.043zbMATH Open1164.68019arXiv0801.1177OpenAlexW2137378957MaRDI QIDQ1017680FDOQ1017680

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

Publication date: 12 May 2009

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

Abstract: We present foundational work on standard bases over rings and on Boolean Groebner bases in the framework of Boolean functions. The research was motivated by our collaboration with electrical engineers and computer scientists on problems arising from formal verification of digital circuits. In fact, algebraic modelling of formal verification problems is developed on the word-level as well as on the bit-level. The word-level model leads to Groebner basis in the polynomial ring over Z/2n while the bit-level model leads to Boolean Groebner bases. In addition to the theoretical foundations of both approaches, the algorithms have been implemented. Using these implementations we show that special data structures and the exploitation of symmetries make Groebner bases competitive to state-of-the-art tools from formal verification but having the advantage of being systematic and more flexible.

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

Recommendations

• Boolean Gröbner bases. Theory, algorithms and applications
• Polybori: A framework for Gröbner-basis computations with Boolean polynomials
• Groebner bases based verification solution for SystemVerilog concurrent assertions
• The Gröbner basis of the ideal of vanishing polynomials
• Boolean Gröbner bases

zbMATH Keywords

polynomial ringBoolean functionsformal verification of digital circuitsstandard bases over ringsBoolean Gröbner bases

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)

Cites Work

• Theory and Applications of Satisfiability Testing
• SATLIB: An online resource for research on SAT
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Converting bases with the Gröbner walk
• Title not available (Why is that?)
• Interpolants and Symbolic Model Checking
• Algorithmic properties of polynomial rings
• Title not available (Why is that?)
• Unique factorization rings with zero divisors
• Unique Factorization Rings with Zero Divisors
• Title not available (Why is that?)
• Title not available (Why is that?)
• A generalization of the Smarandache function to several variables
• Title not available (Why is that?)

Cited In (18)

• Groebner bases based verification solution for SystemVerilog concurrent assertions
• Algebraic verification method for SEREs properties via Groebner bases approaches
• Minimal Gröbner bases and the predictable leading monomial property
• An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths
• Boolean ideals and their varieties
• Role of involutive criteria in computing Boolean Gröbner bases
• Formalization of Dubé's degree bounds for Gröbner bases in Isabelle/HOL
• The Gröbner basis of the ideal of vanishing polynomials
• Cohomology, Bocksteins, and resonance varieties in characteristic 2
• Space Complexity in Polynomial Calculus
• Obtaining and solving systems of equations in key variables only for the small variants of AES
• Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases
• Narrow proofs may be maximally long
• Polybori: A framework for Gröbner-basis computations with Boolean polynomials
• BIBasis, a package for REDUCE and Macaulay2 computer algebra systems to compute Boolean involutive and Gröbner bases
• Model checking technology and tool development based on Groebner base
• On computation of Boolean involutive bases
• Boolean Gröbner bases

Uses Software

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

This page was built for publication: New developments in the theory of Gröbner bases and applications to formal verification

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