Bonsai: cutting models down to size

S. Vijzelaar, K. Verstoep, W. Fokkink, H. Bal

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

2 Citations (Scopus)


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 - 9th International Ershov Informatics Conference, PSI 2014, St. Petersburg, Russia, June 24-27, 2014. Revised Selected Papers
EditorsA Voronkov, I. Virbitskaite
Place of PublicationBerlin
Number of pages15
ISBN (Electronic)978-3-662-46823-4
ISBN (Print)978-3-662-46822-7
Publication statusPublished - 2015
Externally publishedYes
Event9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014) - St. Petersburg, Russian Federation
Duration: 24 Jun 201427 Jun 2014

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference9th International Ershov Informatics Conference on Perspectives of System Informatics, (PSI2014)
Abbreviated titlePSI2014
Country/TerritoryRussian Federation
CitySt. Petersburg
Internet address


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

Cite this