Software model checking, an algorithmic, specification-driven approach to software analysis, has emerged as an active area of research in the last few years, producing a number of successful tools. The central question here is: does a model of a procedural program (typically a context-sensitive or pushdown abstraction) satisfy its requirements (typically expressed using temporal logics or automata)? In this thesis, we study specification formalisms and analysis algorithms applicable to this problem.; We start by observing that classical temporal logics like the mu-calculus or CTL cannot specify "context-sensitive" requirements such as: "If a lock is not held before a call, it must be released before the matching return." A fix, we show, is to model branching behaviors of programs not by computation trees, but by infinite graphs called nested trees. Logics and automata interpreted on these new structures are now defined, and the model checking problem is phrased as: "Does the nested tree generated by a program satisfy a property?" This formulation lets us specify context-sensitive requirements such as pre/post-conditions, "local" dataflow properties, and stack-sensitive access control requirements, and, generally, leads to more modular specifications. Yet, these formalisms are theoretically robust, the complexity of model checking stays the same as before, and symbolic model checking is possible. An application is a specification language (called PAL) that can modularly state context-sensitive safety specifications, and has use in model checking and runtime monitoring of C programs.; On the algorithmic end, we study reachability in pushdown systems, a problem central to software model checking and program analysis that was, for long, believed to intrinsically cubic and behind the cubic bottleneck of its many applications. We offer three subcubic algorithms for this problem, one for the general case, one when the system has no unbounded recursion, and one when there is no recursion at all. The first algorithm views pushdown reachability in a new way---as a computation on sets of system states---and the second algorithm is obtained via a new algorithm for graph transitive closure that is possibly of independent interest. Together, the results identify a gradation in the complexity of the pushdown reachability problem as recursion is restricted.
展开▼
