SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 16:00 - 16:15 at Orchid Small - TOPLAS and Remote Chair(s): Charles Zhang

Binary Decision Diagrams (BDDs) are widely used for the representation of Boolean functions. Context-Free-Language Ordered Decision Diagrams (CFLOBDDs) are a plug-compatible replacement for BDDs—roughly, they are BDDs augmented with a certain form of procedure call. A natural question to ask is, “For a given family of Boolean functions F, what is the relationship between the size of a BDD for and the size of a CFLOBDD for f?” Sistla et al. established that there are best-case families of functions, which demonstrate an inherently exponential separation between CFLOBDDs and BDDs. They showed that there are families of functions for which, for all , the CFLOBDD for (using a particular variable order) is exponentially more succinct than any BDD for (i.e., using any variable order). However, they did not give a worst-case bound—i.e., they left open the question, “Is there a family of functions for which the size of a CFLOBDD for must be substantially larger than a BDD for ?” For instance, it could be that there is a family of functions for which the BDDs are exponentially more succinct than any corresponding CFLOBDDs. This article studies such questions, and answers the second question posed above in the negative. In particular, we show that by using the same variable ordering in the CFLOBDD that is used in the BDD, the size of a CFLOBDD for any function h cannot be far worse than the size of the BDD for h. The bound that relates their sizes is polynomial: If BDD B for function h is of size and uses variable ordering Ord, then the size of the CFLOBDD C for h that also uses Ord is bounded by . The article also shows that the bound is tight: there is a family of functions for which grows as .

Sat 18 Oct

Displayed time zone: Perth change

16:00 - 17:30
TOPLAS and RemoteOOPSLA at Orchid Small
Chair(s): Charles Zhang The Hong Kong University of Science and Technology
16:00
15m
Talk
(TOPLAS) Polynomial Bounds of CFLOBDDs against BDDs
OOPSLA
Xusheng Zhi University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison
DOI
16:15
15m
Talk
(TOPLAS) Type-Safe Compilation of Dynamic Inheritance via Merging
OOPSLA
Yaozhu Sun National Institute of Informatics, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong
16:30
15m
Talk
Detecting and explaining (in-)equivalence of context-free grammars
OOPSLA
Marko Schmellenkamp Ruhr University Bochum, Thomas Zeume Ruhr University Bochum, Sven Argo Ruhr University Bochum, Sandra Kiefer University of Oxford, Cedric Siems Ruhr University Bochum, Fynn Stebel Ruhr University Bochum
16:45
15m
Talk
Modal Abstractions for Virtualizing Memory Addresses
OOPSLA
Ismail Kuru Drexel University, Colin Gordon Drexel University
17:00
15m
Talk
Agora: Trust Less and Open More in Verification for Confidential Computing
OOPSLA
Hongbo Chen Indiana University Bloomington, Quan Zhou Penn State University, Sen Yang Yale University, Dang Sixuan Duke University, Xing Han The Hong Kong University of Science and Technology, Danfeng Zhang Duke University, Fan Zhang Yale University, XiaoFeng Wang Nanyang Technological University
17:15
15m
Talk
QED in Context: An Observation Study of Proof Assistant Users
OOPSLA
Jessica Shi University of Pennsylvania, Cassia Torczon University of Pennsylvania, Harrison Goldstein University at Buffalo, the State University of New York at Buffalo, Benjamin C. Pierce University of Pennsylvania, Andrew Head University of Pennsylvania