Accession Number:

ADA339195

Title:

Compositional Reasoning in Model Checking

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

1998-02-02

Pagination or Media Count:

21.0

Abstract:

The main problem in model checking that prevents it from being used for verification of large systems is the state explosion problem. This problem often arises from combining parallel processes together. Many techniques have been proposed to overcome this difficulty and thus increase the size of the systems that model checkers can handle. We describe several compositional model checking techniques used in practice and show a few examples demonstrating their performance.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE