Analysis of Boolean Programs

Boolean programs are a popular abstract domain for static-analysis-based software model checking. Yet little is known about the complexity of model checking for this model of computation. This paper aims to fill this void by providing a comprehensive study of the worst-case complexity of several basic analyses of Boolean programs, including reachability analysis, cycle detection, LTL, CTL and CTL* model checking. We present algorithms for these problems and show that our algorithms are all {\em optimal} by providing matching lower bounds. We also identify particular classes of Boolean programs which are easier to analyse, and compare our results to prior work on context-free and pushdown model checking.

PDF file


> Publications > Analysis of Boolean Programs