Bonsai: Cutting models down to size

S.J.J. Vijzelaar*, K. Verstoep, H.E. Bal, W.J. Fokkink

*Corresponding author for this work

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


In model checking, abstractions can cause spurious results, which need to be verified in the concrete system to gain conclusive results. Verification based on multi-valued model checking can distinguish conclusive and inconclusive results, while increasing precision over traditional two-valued over- and under-abstractions. This paper describes the theory and implementation of multi-valued model checking for Promela specifications. We believe our tool Bonsai is the first four-valued model checker capable of multi-valued verification of parallel models, i.e. consisting of multiple concurrent processes. A novel aspect is the ability to only partially abstract a model, keeping parts of it concrete.

Original languageEnglish
Title of host publicationPerspectives of System Informatics
Subtitle of host publication9th International Ershov Informatics Conference, PSI 2014, Revised Selected Papers
EditorsIrina Virbitskaite, Andrei Voronkov, Irina Virbitskaite
PublisherSpringer - Verlag
Number of pages15
ISBN (Electronic)9783662468234
ISBN (Print)9783662468227
Publication statusPublished - 2015
Event9th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2014 - St. Petersburg, Russian Federation
Duration: 24 Jun 201427 Jun 2014

Publication series

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


Conference9th International Ershov Informatics Conference on Perspectives of System Informatics, PSI 2014
Country/TerritoryRussian Federation
CitySt. Petersburg


Dive into the research topics of 'Bonsai: Cutting models down to size'. Together they form a unique fingerprint.

Cite this