Mathematics – Commutative Algebra
Scientific paper
2008-01-08
Mathematics
Commutative Algebra
44 pages, 8 figures, submitted to the Special Issue of the Journal of Pure and Applied Algebra
Scientific paper
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.
Brickenstein Michael
Dreyer Alexander
Greuel Gert-Martin
Wedler Markus
Wienand Oliver
No associations
LandOfFree
New developments in the theory of Groebner bases and applications to formal verification does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with New developments in the theory of Groebner bases and applications to formal verification, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and New developments in the theory of Groebner bases and applications to formal verification will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-420786