Home > Research > Publications & Outputs > PBMC

Associated organisational unit

Links

Text available via DOI:

View graph of relations

PBMC: Symbolic slicing for the verification of concurrent programs

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Published
Close
NullPointerException

Abstract

This paper proposes a novel optimization of bounded model checking (BMC) for better run-time efficiency. Specifically, we define projections, an adaptation of dynamic program slices, and instruct the bounded model checker to check projections only. Given state properties over a subset of the program’s variables, we prove the soundness of the proposed optimization. We propose a symbolic encoding of projections and implement it for a prototype language of concurrent programs. We have developed a tool called PBMC to evaluate the efficiency of the proposed approach. Our evaluation with various concurrent programs justifies the potential of projections to efficient verification. © Springer International Publishing Switzerland 2015.