Home > Research > Publications & Outputs > PBMC

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

Standard

PBMC : Symbolic slicing for the verification of concurrent programs. / Saissi, H.; Bokor, P.; Suri, Neeraj.

Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. Vol. 9364 Springer-Verlag, 2015. p. 344-360.

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

Harvard

Saissi, H, Bokor, P & Suri, N 2015, PBMC: Symbolic slicing for the verification of concurrent programs. in Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. vol. 9364, Springer-Verlag, pp. 344-360. https://doi.org/10.1007/978-3-319-24953-7_26

APA

Saissi, H., Bokor, P., & Suri, N. (2015). PBMC: Symbolic slicing for the verification of concurrent programs. In Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings (Vol. 9364, pp. 344-360). Springer-Verlag. https://doi.org/10.1007/978-3-319-24953-7_26

Vancouver

Saissi H, Bokor P, Suri N. PBMC: Symbolic slicing for the verification of concurrent programs. In Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. Vol. 9364. Springer-Verlag. 2015. p. 344-360 https://doi.org/10.1007/978-3-319-24953-7_26

Author

Saissi, H. ; Bokor, P. ; Suri, Neeraj. / PBMC : Symbolic slicing for the verification of concurrent programs. Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. Vol. 9364 Springer-Verlag, 2015. pp. 344-360

Bibtex

@inbook{be53637686ae462183049afc47fbab13,
title = "PBMC: Symbolic slicing for the verification of concurrent programs",
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{\textquoteright}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. {\textcopyright} Springer International Publishing Switzerland 2015.",
keywords = "Efficiency, Bounded model checkers, Bounded model checking, Concurrent program, Dynamic programs, Run-time efficiency, Model checking",
author = "H. Saissi and P. Bokor and Neeraj Suri",
year = "2015",
doi = "10.1007/978-3-319-24953-7_26",
language = "English",
isbn = "9783319249520",
volume = "9364",
pages = "344--360",
booktitle = "Automated Technology for Verification and Analysis",
publisher = "Springer-Verlag",

}

RIS

TY - CHAP

T1 - PBMC

T2 - Symbolic slicing for the verification of concurrent programs

AU - Saissi, H.

AU - Bokor, P.

AU - Suri, Neeraj

PY - 2015

Y1 - 2015

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

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

KW - Efficiency

KW - Bounded model checkers

KW - Bounded model checking

KW - Concurrent program

KW - Dynamic programs

KW - Run-time efficiency

KW - Model checking

U2 - 10.1007/978-3-319-24953-7_26

DO - 10.1007/978-3-319-24953-7_26

M3 - Chapter

SN - 9783319249520

VL - 9364

SP - 344

EP - 360

BT - Automated Technology for Verification and Analysis

PB - Springer-Verlag

ER -