Publica
Hier finden Sie wissenschaftliche Publikationen aus den FraunhoferInstituten. Networkdriven boolean normal forms
 Becker, B.: Verification over discretecontinuous boundaries : Dagstuhl Seminar 10271, 04.07.  09.07.2010 Wadern: Schloss Dagstuhl ? LeibnizZentrum für Informatik GmbH, 2010 (Dagstuhl Seminar Proceedings 10271) ISSN: 18624405 8 pp. 
 Dagstuhl Seminar "Verification Over DiscreteContinuous Boundaries" <2010, Schloss Dagstuhl> 

 English 
 Conference Paper, Electronic Publication 
 Fraunhofer ITWM () 
Abstract
We apply the PolyBoRi framework for Groebner bases computations with Boolean polynomials to bitvalued problems from algebraic cryptanalysis and formal verification. First, we proposed zerosuppressed binary decision diagrams (ZDDs) as a suitable data structure for Boolean polynomials. Utilizing the advantages of ZDDs we develop new reduced normal form algorithms for linear lexicographical lead rewriting systems. The latter play an important role in modeling bitvalued components of digital systems. Next, we reorder the variables in Boolean polynomial rings with respect to the topology of digital components. This brings computational algebra to digital circuits and small scale crypto systems in the first place. We additionally propose an optimized topological ordering, which tends to keep the intermediate results small. Thus, we successfully applied the linear lexicographical lead techniques to nontrivial examples from formal verification of digital systems. Finally, we evaluate the performance using benchmark examples from formal verification and cryptanalysis including equivalence checking of a bitlevel formulation of multiplier components. Before we introduced topological orderings in PolyBoRi, state of the art for the algebraic approach was a bitwidth of 4 for each factor. By combining our techniques we raised this bound to 16, which is an important step towards realworld applications.