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

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)

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.

Recommendations

Cites work

Cited in

(18)

Describes a project that uses

Uses Software

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)