Technical Report CS718

Authors: G. Shurek and O. Grumberg
PDFNot Available

This paper presents a modular, semi-automatic method for the verification of finite-state programs with temporal logic specifications, based on model checking procedures. The purpose of this work, however, goes beyond the search for a technical solution to modular verification. The additional goal is to gain a wider understanding of the modular framework. Most of the introduction is dedicated to a general discussion of this framework - motivation, solutions and evaluation criteria. Previous works in this are are discussed in that context. Moreover, throughout the paper results are related to this discussion.

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 or PS files directly. The latter URLs may change without notice.

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

Computer science department, Technion