首页 | 本学科首页   官方微博 | 高级检索  
     检索      


New developments in the theory of Gröbner bases and applications to formal verification
Authors:Michael Brickenstein  Markus Wedler
Institution:a Mathematisches Forschungsinstitut Oberwolfach, Schwarzwaldstr. 9-11, 77709 Oberwolfach-Walke, Germany
b Fraunhofer Institute for Industrial Mathematics (ITWM), Fraunhofer-Platz 1, 67663 Kaiserslautern, Germany
c University of Kaiserslautern, Erwin-Schrödinger-Straße, 67653 Kaiserslautern, Germany
Abstract: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 basis in the polynomial ring over Z/2n 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.
Keywords:Primary  06E20  13F20  13P10  secondary  13B25  13F15  13M10  33F10  68W30
本文献已被 ScienceDirect 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号