Home > Research > Publications & Outputs > PBMC


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

Publication date2015
Host publicationAutomated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings
Number of pages17
ISBN (Print)9783319249520
<mark>Original language</mark>English


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.