Computer Science Colloquium
Dr. Robert Meolic
Faculty of Electrical Engineering and Computer Science, University of Maribor, Slovenia
Implementation Aspects of a BDD Package Supporting General Decision Diagrams
Mon 19.09.2016, 10:00, 60 minutesS3 058, Computer Science Building (Science Park 3)
Abstract
A 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.
Bio
Robert Meolic received his Ph.D from the University of Maribor, Slovenia in 2005. He is currently an Assistant Professor at the Faculty of Electrical Engineering and Computer Science at the same university. He is involved in teaching Digital Circuits Design, Programming in C++, and Software Engineering. His main research interests include Boolean Algebra, Binary Decision Diagrams, Temporal Logic and Model Checking. He is a main maintainer of two academic computer tools, a BDD package Biddy and a toolbox for formal verification of systems EST.Invited by Univ.-Prof. Dr. Robert Wille, Institut für Integrierte Schaltungen, Abteilung Integrierter Schaltungs- und Systementwurf
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).