×

zbMATH — the first resource for mathematics

New developments in the theory of Gröbner bases and applications to formal verification. (English) Zbl 1164.68019
Summary: We present foundational work on standard bases over rings and on Boolean Gröbner 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 Gröbner bases in the polynomial ring over \(\mathbb Z/2^n\) while the bit-level model leads to Boolean Gröbner 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 Gröbner bases competitive to state-of-the-art tools from formal verification but having the advantage of being systematic and more flexible.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
06E30 Boolean functions
13F20 Polynomial rings and ideals; rings of integer-valued polynomials
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
68W30 Symbolic computation and algebraic computation
94C10 Switching theory, application of Boolean algebra; Boolean functions (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] McMillan, K.L., Symbolic model checking, (1993), Kluwer Academic Publishers Norwell, MA, USA · Zbl 1132.68474
[2] Hachtel, G.D.; Somenzi, F., Logic synthesis and verification algorithms, (1996), Kluwer Academic · Zbl 0861.94035
[3] Kunz, W.; Marques-Silva, J.; Malik, S., SAT and ATPG: algorithms for Boolean decision problems, (), 309-341
[4] Smith, D.J., VHDL & verilog compared & contrasted – plus modeled example written in VHDL, verilog and C, (), 771-776
[5] O. Wienand, The Groebner basis of the ideal of vanishing polynomials, arXiv:0709.2978v1[math.AC]
[6] O. Wienand, Ph.D Thesis, University of Kaiserslautern, Germany (2009) (in preparation)
[7] Adams, W.; Loustaunau, P., An introduction to Gröbner bases, () · Zbl 0803.13015
[8] Kalkbrener, M., Algorithmic properties of polynomial rings, J. symbolic comput., 26, 5, 525-581, (1998) · Zbl 0920.68129
[9] Greuel, G.-M.; Pfister, G., A singular introduction to commutative algebra, (2002), Springer
[10] Becker, T.; Weispfennig, V., Gröbner bases, a computational approach to commutative algebra, ()
[11] Agargün, A.G., Unique factorization rings with zero divisors, Comm. algebra, 27, 4, 1967-1974, (1999) · Zbl 0947.13013
[12] Galovich, S., Unique factorization rings with zero-divisors, Math. mag., 51, 276-283, (1978) · Zbl 0407.13013
[13] Bouvier, A., Structure des anneaux a factorisation unique, Publ. dep. math. (Lyon), 11, 39-49, (1974) · Zbl 0294.13013
[14] Fletcher, C.R., Unique factorization rings, Proc. Cambridge phil. soc., 65, 3, 579-583, (1969) · Zbl 0174.33401
[15] Zariski, O.; Samuel, P., ()
[16] Norton, G.H.; Salagean, A., Strong Gröbner bases for polynomials over a principal ideal ring, Bull. austral. math. soc., 66, 145-152, (2002)
[17] M. Ghasemzadeh, A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memorization, Ph.D. Thesis, University of Potsdam, Potsdam, Germany, Nov. 2005. http://opus.kobv.de/ubp/volltexte/2006/637/
[18] Bérard, B.; Bidoit, M.; Laroussine, F.; Petit, A.; Petrucci, L.; Schoenebelen, P.; McKenzie, P., Systems and software verification: model-checking techniques and tools, (1999), Springer-Verlag New York, Inc. New York, NY, USA
[19] S. Minato, Implicit manipulation of polynomials using zero-suppressed BDDs, in: Proc. of IEEE The European Design and Test Conference, ED&TC’95, 1995, pp. 449-454
[20] Bachmann, O.; Schönemann, H., Monomial representations for Gröbner bases computations, (), 309-316 · Zbl 0924.68104
[21] M. Brickenstein, A. Dreyer, PolyBoRi: A framework for Gröbner basis computations with boolean polynomials, Electronic Proceedings of Effective Methods in Algebraic Geometry MEGA 2007, 2007. http://www.ricam.oeaw.ac.at/mega2007/electronic/26.pdf
[22] M. Brickenstein, Slimgb: Gröbner Bases with Slim Polynomials, in: Rhine Workshop on Computer Algebra, 2006, pp. 55-66, Proc. RWCA’06, Basel, March 2006
[23] Giovini, A.; Mora, T.; Niesi, G.; Robbiano, L.; Traverso, C., One sugar cube, please or selection strategies in buchberger algorithms, (), 49-54 · Zbl 0933.68161
[24] G.-M. Greuel, G. Pfister, H. Schönemann, SINGULAR 3.0, A Computer Algebra System for Polynomial Computations, Centre for Computer Algebra, University of Kaiserslautern, 2005. http://www.singular.uni-kl.de
[25] Hungerbühler, N.; Specker, E., A generalization of the smarandache function, integers, Electronic J. combinatorial number theory, 6, (2006), #A23 · Zbl 1114.11003
[26] F. Somenzi, CUDD: CU decision diagram package, University of Colorado at Boulder, release 2.4.1 (2005). URL http://vlsi.colorado.edu/ fabio/CUDD/
[27] A.A. Stepanov, M. Lee, The Standard Template Library, Tech. Rep. X3J16/94-0095, WG21/N0482, 1994
[28] Rossum, G.V.; Drake, F.L., The python language reference manual, (2006), Network Theory Ltd Bristol, United Kingdom
[29] W. Stein, SAGE Mathematics Software, The SAGEGroup (2007). http://www.sagemath.org
[30] Collart, S.; Kalkbrener, M.; Mall, D., Converting bases with the Gröbner walk, J. symbolic comput., 24, 465-469, (1997) · Zbl 0908.13020
[31] Hoos, H.H.; Stützle, T., SATLIB: an online resource for research on SAT, (), 283-292 · Zbl 0979.68128
[32] Eén, N.; Sörensson, N., An extensible SAT-solver, (), 502-518 · Zbl 1204.68191
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.