×

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)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] McMillan, K. L., Symbolic Model Checking (1993), Kluwer Academic Publishers: 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, (Hassoun, S.; Sasao, T., Logic Synthesis and Verification. Logic Synthesis and Verification, The Springer International Series in Engineering and Computer Science, vol. 654 (2002), Kluwer Academic Publishers: Kluwer Academic Publishers Norwell, MA, USA), 309-341
[4] Smith, D. J., VHDL & Verilog compared & contrasted-Plus modeled example written in VHDL, Verilog and C, (DAC ’96: Proceedings of the 33rd Annual Conference on Design Automation (1996), ACM Press: ACM Press New York, NY, USA), 771-776
[5] O. Wienand, The Groebner basis of the ideal of vanishing polynomials, arXiv:0709.2978v1; O. Wienand, The Groebner basis of the ideal of vanishing polynomials, arXiv:0709.2978v1
[6] O. Wienand, Ph.D Thesis, University of Kaiserslautern, Germany (2009) (in preparation); O. Wienand, Ph.D Thesis, University of Kaiserslautern, Germany (2009) (in preparation)
[7] Adams, W.; Loustaunau, P., An introduction to Gröbner bases, (Graduate Studies in Mathematics (2003), AMS) · 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, (Graduate Texts in Mathematics (1993), Springer Verlag)
[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., (Commutative Algebra, Vol. I. Commutative Algebra, Vol. I, Graduate Texts in Mathematics, vol. 28 (1979), Springer) · Zbl 0112.02902
[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/; 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.: 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; 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, (Proc. of the International Symposium on Symbolic and Algebraic Computation. Proc. of the International Symposium on Symbolic and Algebraic Computation, ISSAC’98 (1998), ACM Press), 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; 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; 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, (Watt, S., Proceedings of the 1991 International Symposium on Symbolic and Algebraic Computations. Proceedings of the 1991 International Symposium on Symbolic and Algebraic Computations, ISSAC’91 (1991), ACM Press), 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; 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/; 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; 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: Network Theory Ltd Bristol, United Kingdom
[29] W. Stein, SAGE Mathematics Software, The SAGEGroup (2007). http://www.sagemath.org; 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, (Gent, I. P.; Maaren, H.v.; Walsh, T., SAT 2000 (2000), IOS Press), 283-292 · Zbl 0979.68128
[32] Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., SAT. SAT, Lecture Notes in Computer Science, vol. 2919 (2003), Springer), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.