Compositional Reasoning in Model Checking

The main problem in model checking that prevents it from being used for veri cation 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 di culty and, thus, increase the size of the systems that model checkers can handle. We describe several compositionalmodel checkingtechniques used in practice and show a few examples demonstrating their performance.

• Type: Conference
• Year: 1997
• Where: COMPOS
• Authors: Sergey Berezin, Sérgio Vale Aguiar Campos, Edmund M. Clarke
• Keywords: COMPOS 1997, Formal Methods, Main Problem, State Explosion Problem, Veri Cation