Computer Science ColloquiumIm Rahmen des Informatik-Kolloquiums, das von den Instituten des Fachbereichs Informatik, der Österreichischen Gesellschaft für Informatik (ÖGI), der Arbeitsgemeinschaft für Datenverarbeitung (ADV) sowie der Österreichischen Computergesellschaft (OCG) abgehalten wird, spricht
Dr. Robert Meolic
Faculty of Electrical Engineering and Computer Science, University of Maribor, Sloveniaüber das Thema:
Implementation Aspects of a BDD Package Supporting General Decision DiagramsZeit: 2016-09-19 10:00:00.0, 60 Minuten
Ort: S3 058, Computer Science Building (Science Park 3)
ZusammenfassungA binary decision diagram (BDD) is a directed, acyclic, binary graph with one root. Originally, BDDs were introduced in the field of digital circuit design as a data structure for efficient representation of Boolean functions. Efficient implementations started to appear in the beginning of '90s. Nowadays, BDDs are also applied to model checking and other verification methods, reachability and reliability analysis, automated reasoning, various combinatorial problems, and many other fields.
A BDD package is a computer library which allows other software to create and manipulate BDDs. All created BDDs are represented simultaneously, and they share as many nodes as possible. Internally, BDD packages use common mechanisms for efficiency: a hash table to store nodes, multiple caches to store already computed results, and heuristic strategies for memory management. Furthermore, a BDD package may offer a manager which allows calculations as if there were multiple copies of the system, i.e. BDDs in different groups do not share nodes and also all internal structures are duplicated. Well-known non-proprietary BDD packages are CUDD and BuDDy.
In the talk, the BDD package Biddy which is developed at the University of Maribor (Slovenia) is introduced. Biddy provides a comprehensible API and an original implementation of memory management. The talk will introduce the functionalities and implementation details of the current version of Biddy. Interesting parts will be explained by live demonstrations. General decision diagrams will be discussed on a theoretical level.