CMU-CS-98-106
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-98-106

Compositional Reasoning in Model Checking

Sergey Berezin, Sergio Campos*, Edmund M. Clarke

February 1998

[To appear in the Proceedings of the Workshop COMPOS'97.]

CMU-CS-98-106.ps


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.

Keywords: Automatic verification, temporal logic, compositional model checking, bisimulation


21 pages

*Universidade Federal de Minas Gerais, Brazil

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu