Brief description:

Within the research field of BDD-based data structures for Boolean functions data structures, for the representation and computation of Boolean (i.e., 0-1-valued) functions have been designed and analyzed . The various practical applications of such data structures, e.g., in CAD systems for circuit design or in tools for the formal verification of communication protocols, sequential systems or electronic circuits made optimization and compactification of such structures a very worthwhile aim of research.

Research Topics

• Optimizing OBDDs
  • Development of new global reordering strategies for minimization of OBDDs.
  • State encoding of sequential systems
  • Reduction concepts
• More powerful BDD concepts
  • Free BDDs
  • Transformation concepts
  • Probabilistic Verification Using Parity-OBDDs
• BDDs in applications
  • Accelerating the Variable Reordering Process
  • OHO: OBDD-Heuristics Online: BDD-heuristic evaluation via WWW
  • Algorithms for BDDs with different variable orders
  • Partitioning of Transition Relations
• BDDs in logic
  • ZQSAT: a QSAT solver based on ZDDs.

Our Publications

• ... on BDDs and their application in digital system design and formal verification
• ... the full text version of our OBDD-book (Christoph Meinel/Torsten Theobald)

PhD-Theses

• "A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoizationinen"
  by Mohammed Ghasemzadeh, 2006
• "High-level Methods for OBDD-based Sequential Verification"
  by Christian Stangier, 2002
• "Improving the Power of Ordered Binary Decision Diagrams by Integrating Parity Nodes"
  by Harald Sack, 2002
• "Transformation Techniques for Decision Diagrams in Computer-Aided Design"
  by Thorsten Theobald, 1997

People

• Team leader:
• Prof. Dr. Christoph Meinel
• Former members:
• Dr. rer. nat. Mohammad Ghasemzadeh
• Dipl.-Inform. Volker Klotz
• Dr. Rustam Mubarakzjanov (now with Kazan University)
• Dr. rer. nat. Christian Stangier (now with Fujitsu, USA)
• Dr. rer. nat. Harald Sack (now with Uni Jena)
• Dipl.-Math.Jochen Bern (now with IT-Services, Luxembourg)
• Dipl. Inform. Jordan Gergov (now with MPI Saarbrücken)
• Dr. Anna Slobodova (now with Compaq, Boston)
• Prof. Dr. rer. nat. Thorsten Theobald (now with TU München)
• Dipl. Inform. Arno Wagner (now with ETH Zürich)

Some other activities:

• We offer and maintain for BDD-researcher's community the www-portal www.bdd-portal.org, that links all researchers, conferences and workshops in the area, as well as provides access to tools and benchmarks, and permits online evaluation and test of BDD-based software tools.
• We co-organised the serious of Dagstuhl-seminars on Design and Test:
  2001 - 1999 - 1997 - 1995

Common Projects and Cooperations with

• Institute of Telematics, Trier
• Politecnico Torino
• University of Colorado at Boulder
• DFG-Research Cluster  Efficient Algorithms for discrete problems and their applications
• DFG Graduiertenkolleg MathematischeOptimierung
• DIGITAL
• Fujitsu Labs, San Jose
• IBM
• SIEMENS
• SYNOPSYS