Edge-Specified Reduction Binary Decision Diagrams
Various versions of binary decision diagrams (BDDs) have been proposed in the past, differing in the reduction rule needed to interpret the meaning of edges skipping levels. The most widely adopted, fully-reduced BDDs and zero-suppressed BDDs, excel at encoding different types of boolean functions (the former when the function has many “don’t-care”, the latter when it tends to have value zero when one of its arguments is nonzero). Recently, new classes of BDDs have been proposed that, at the cost of some additional complexity and larger memory requirements per node, attempt to exploit both cases. We introduce a new type of BDD that we believe is conceptually simpler, yet has small memory requirements in terms of node size, tends to result in fewer nodes, and can easily be extended to include further reduction rules. We present a formal definition, prove canonicity, and provide experimental results to support our efficiency claims.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:30 - 18:00 | |||
16:30 30mTalk | iRank: a variable order metric for DEDS subject to linear invariants TACAS Link to publication | ||
17:00 30mTalk | Edge-Specified Reduction Binary Decision Diagrams TACAS Link to publication | ||
17:30 30mTalk | Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS Jens Katelaan , Christoph Matheja RWTH Aachen University, Florian Zuleger Vienna University of Technology Link to publication |