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/ISSN › Chapter
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_26APA
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_26Vancouver
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 -
