Paper Info
Title
Closure operators for ROBDDs
Abstract
Program analysis commonly makes use of Boolean functions to express information about run-time states. Many important classes of Boolean functions used this way, such as the monotone functions and the Boolean Horn functions, have simple semantic characterisations. They also have well-known syntactic characterisations in terms of Boolean formulae, say, in conjunctive normal form. Here we are concerned with characterisations using binary decision diagrams. Over the last decade, ROBDDs have become popular as representations of Boolean functions, mainly for their algorithmic properties. Assuming ROBDDs as representation, we address the following problems: Given a function ψ and a class of functions Δ, how to find the strongest ϕεΔ entailed by ψ (when such a ϕ is known to exist)? How to find the weakest ϕεΔ that entails ψ? How to determine that a function ψ belongs to a class Δ? Answers are important, not only for several program analyses, but for other areas of computer science, where Boolean approximation is used. We give, for many commonly used classes Δ of Boolean functions, algorithms to approximate functions represented as ROBDDs, in the sense described above. The algorithms implement upper closure operators, familiar from abstract interpretation. They immediately lead to algorithms for deciding class membership.
Year
DOI
Venue
2006
10.1007/11609773_1
VMCAI
Keywords
Field
DocType
boolean function,closure operator,boolean formula,simple semantic characterisations,well-known syntactic characterisations,program analysis,class membership,approximate function,important class,boolean approximation,boolean horn function,monotone function,conjunctive normal form,binary decision diagram
Boolean network,Boolean function,Maximum satisfiability problem,Discrete mathematics,Stone's representation theorem for Boolean algebras,Boolean circuit,Computer science,Parity function,Product term,Boolean expression
Conference
Volume
ISSN
ISBN
3855
0302-9743
3-540-31139-4
Citations 
PageRank 
References 
4
0.42
15
Authors
2
Name
Order
Citations
PageRank
Peter Schachte125622.76
Harald Søndergaard285879.52