Compositional model checking with incremental counter-example construction

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)


In compositional model checking, the approach is to reason about the correctness of a system by lifting results obtained in analyses of subsystems to the system-level. The main challenge, however, is that requirements, in the form of temporal logic formulae, are usually specified at the system-level, and it is not obvious how to relate these to subsystem-local behaviour. In this paper, we propose a new approach to checking regular safety properties, which we call Incremental CounterExample Construction (ICC). Its main strong point is that it performs a series of model checking procedures, and that each one only explores a small part of the entire state space. This makes ICC an excellent approach in those cases where state space explosion is an issue. Moreover, it is frequently much faster than traditional explicit-state model checking, particularly when the model satisfies the verified property, and in most cases not significantly slower. We explain the technique, and report on experiments we have conducted using an implementation of ICC, comparing the results to those obtained with other approaches.

Original languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I
EditorsR. Majumdar, V. Kunčak
Place of PublicationDordrecht
Number of pages21
ISBN (Print)9783319633862
Publication statusPublished - 2017
Event29th International Conference on Computer Aided Verification, CAV 2017 - Heidelberg, Germany
Duration: 24 Jul 201728 Jul 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10426 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference29th International Conference on Computer Aided Verification, CAV 2017


Dive into the research topics of 'Compositional model checking with incremental counter-example construction'. Together they form a unique fingerprint.

Cite this