Grafting a Promela front-end with abstract data types to mitigate the sensitivity of (compositional) analysis to implementation choices

Research output: Contribution to journalConference articlepeer-review

1 Scopus citations


Recently, an active research topic in software verification is applying model checkers to programs, such as multi-threaded Java code. However, a program typically consists of more behaviors, such as operations on complicated data structures or implementation details which are typically made for some criteria like performance. A brute-force model extraction may produce a poor model for analysis engine. In this paper, we give examples to show how subtle changes in implementation may result in considerable differences in analysis, particularly to compositional analysis. Unfortunately, these implementation choices are made by programmers - people who typically do not possess the knowledge of verification. To mitigate such sensitivity, we advocate that verification tools should recognize and support abstract data types and, in the meantime, prohibit or suppress the use of array. Programming process behaviors with abstract data types can hide and converge the implementation choices. More importantly, abstract data types are informative. They provide essential information for tool automation to select a best implementation for analysis. In this paper, we describe the design and implementation of such a prototype tool which can parse systems written in Promela syntax.

Original languageEnglish
Pages (from-to)139-153
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - 2005
Event12th International SPIN Workshop on Model Checking Software - San Francisco, CA, United States
Duration: 22 Aug 200524 Aug 2005


Dive into the research topics of 'Grafting a Promela front-end with abstract data types to mitigate the sensitivity of (compositional) analysis to implementation choices'. Together they form a unique fingerprint.

Cite this