One fundamental question needed for verifying safety properties in programs is reachability: Can the program reach a bad state? Precise reachability analysis a computationally hard problem even when restricted to Boolean programs. Therefore, any practical analysis must over-approximate the exact set of reachable program states. Traditional reachability analysis approaches are based on either binary decision diagrams (BDDs) or Boolean satisfiability (SAT) solvers. These approaches have the drawback that they can use exponential space in the number of variables in the program (BDDs), or take exponential time in the size of the program (SAT).

In this work, we present a new formulation to perform over-approximating reachability analysis for Boolean programs in \emph{polynomial time}. Our key insight is to leverage a recent graph reachability formulation called linear-conjunctive language reachability (LCL-reachability) for program analysis. We develop a new graph representation (LCLGRAPH) to \emph{precisely} model Boolean program semantics. In particular, the size of LCLGRAPH is \emph{linear} to the size of the input Boolean program. Given a graph with $n$ nodes and $m$ edges, LCL-reachability algorithm can compute an over-approximating solution in $O(mn)$ time. Therefore, our new framework can provide answers to unreachability queries on Boolean programs with polynomial space and time.