Logics and algorithms for software model checking

2007 2007

Other formats: Order a copy

Abstract (summary)

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 μ-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.

Indexing (details)

Computer science
0984: Computer science
Identifier / keyword
Applied sciences, Model checking, Software, Specification languages
Logics and algorithms for software model checking
Chaudhuri, Swarat
Number of pages
Publication year
Degree date
School code
DAI-B 68/07, Dissertation Abstracts International
Place of publication
Ann Arbor
Country of publication
United States
Alur, Rajeev
University of Pennsylvania
University location
United States -- Pennsylvania
Source type
Dissertations & Theses
Document type
Dissertation/thesis number
ProQuest document ID
Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.
Document URL
Access the complete full text

You can get the full text of this document if it is part of your institution's ProQuest subscription.

Try one of the following:

  • Connect to ProQuest through your library network and search for the document from there.
  • Request the document from your library.
  • Go to the ProQuest login page and enter a ProQuest or My Research username / password.