Sciweavers

Share
SPIN
2010
Springer

Context-Bounded Translations for Concurrent Software: An Empirical Evaluation

8 years 10 months ago
Context-Bounded Translations for Concurrent Software: An Empirical Evaluation
Abstract. Context-Bounded Analysis has emerged as a practical automatic formal analysis technique for fine-grained, shared-memory concurrent software. Two recent papers (in CAV 2008 and 2009) have proposed ingenious translation approaches that promise much better scalability, backed by compelling, but differing, theoretical and conceptual advantages. Empirical evidence comparing the translations, however, has been lacking. Furthermore, these papers focused exclusively on Boolean model checking, ignoring the also widely used paradigm of verification-condition checking. In this paper, we undertake a methodical, empirical evaluation of the three main source-to-source translations for context-bounded analysis of concurrent software, in a verification-condition-checking paradigm. We evaluate their scalability under a wide range of experimental conditions. Our results show: (1) The newest, CAV 2009 translation is the clear loser, with the CAV 2008 translation the best in most instances, b...
Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric
Added 30 Jan 2011
Updated 30 Jan 2011
Type Journal
Year 2010
Where SPIN
Authors Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric
Comments (0)
books