Efficient approximate verification of Promela models via symmetry markers

D. Bosnacki, A.F. Donaldson, M. Leuschel, T. Massart

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

5 Citations (Scopus)
2 Downloads (Pure)


We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a complete verification method which only partially exploits symmetry, and an approximate verification method which fully exploits symmetry. We describe how symmetry markers can be efficiently computed and integrated into the Spin tool, and provide an empirical evaluation of our technique using the Topspin symmetry reduction package, which shows very good performance results and a high degree of precision for the approximate method (i.e. very few non-symmetric states receive the same marker). We also identify a class of models for which the approximate technique is precise.
Original languageEnglish
Title of host publicationProceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan
EditorsK.S. Namjoshi, T. Yoneda, T. Higashino, Y. Okamura
Place of PublicationBerlin, Germany
ISBN (Print)978-3-540-75595-1
Publication statusPublished - 2007
Eventconference; ATVA 2007, Tokyo, Japan; 2007-10-22; 2007-10-25 -
Duration: 22 Oct 200725 Oct 2007

Publication series

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


Conferenceconference; ATVA 2007, Tokyo, Japan; 2007-10-22; 2007-10-25
OtherATVA 2007, Tokyo, Japan

Cite this