Technical Report CS0903

Title: Compositional Model Checking of Software
Authors: Karen Laster and Orna Grumberg
PDFNot Available
Abstract: This work presents a modular approach to temporal logic model checking of software. Model checking is a method that automatically determines whether a finite state system satisfies a temporal logic specification. Model checking algorithms have been successfully used to verify complex systems. However, their use is limited by the high space requirements needed to represent the verified system. When hardware designs are considered, a typical solution is to partition the design into units running in parallel, and handle each unit separately. For software systems such a solution is not always feasible. This is because a software system might be too large to fit into memory even when it consists of a single sequential unit. To avoid the high space requirements for software we suggest to partition the program text into sequentially composed subprograms. Based on this partition, we present a model checking algorithm for software that arrives at its conclusion by examining each subprograms in separation. The novelty of our approach is that it uses a decomposition of the program in which the interconnection between parts is sequential and not parallel. We handle each part separately, while keeping all other parts in an external memory. Consequently, our approach reduces space requirements and enables verification of larger systems. Our method is applicable to finite state programs. Further, it is applicable to infinite state programs provided that a suitable abstraction can be constructed. We consider this work as a first step towards making temporal logic model checking useful for software verification.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 1997
To the main CS technical reports page

Computer science department, Technion