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...

• Type: Journal
• Year: 2010
• Where: SPIN
• Authors: Naghmeh Ghafari, Alan J. Hu, Zvonimir Rakamaric
• Keywords: Boolean Model, Concurrent Software, SPIN 2010, Theoretical Computer Science, Translations