Paper on context-bounded analysis accepted at SPIN 2010


The work I did with Naghmeh and Alan on empirical evaluation of context-bounded translations for concurrent software was accepted at SPIN 2010. We investigate source-to-source translations: a concurrent program, given a bound on the number of context switches, is translated into a corresponding sequential program. In the paper, we compare three different translations in the verification-condition-checking (using SMT solvers) paradigm. We evaluate their scalability under a wide range of experimental conditions: we draw interesting conclusions and provide practical guidance for using context-bounded analysis in a VC-checking paradigm.

The final version of this paper is available here.

And here is what Shaz Qadeer said about the paper: “I really like the paper, quite independent of its focus on evaluation of context-bounded translations. There are very nice insights in the paper about the difference between finite-state symbolic model checking and the VC-based techniques. In fact, I would recommend this paper to anybody who has a model checking background and is beginning to use theorem provers.” Thanks a lot Shaz!

You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.

Comments are closed.