Showing cs.LOShow all
2 papers · 1 filter
cs.LO2018
BDDs Naturally Represent Boolean Functions, and ZDDs Naturally Represent Sets of Sets
Kensuke Kojima
This paper studies a difference between Binary Decision Diagrams (BDDs) and Zero-suppressed BDDs (ZDDs) from a conceptual point of view. It is commonly understood that a BDD is a r…
cs.LO2017
Sharper and Simpler Nonlinear Interpolants for Program Verification
Takamasa Okudono, Yuki Nishida, Kensuke Kojima +3
Interpolation of jointly infeasible predicates plays important roles in various program verification techniques such as invariant synthesis and CEGAR. Intrigued by the recent resul…