Proceedings paper

Title:
Dead Variable Analysis for Multi-threaded Heap Manipulating Programs
Authors:
Pavel Jančík, Jan Kofroň
Publication:
Proceedings of the 31st Annual ACM Symposium on Applied Computing
DOI:
Year:
2016
ISBN:
978-1-4503-3739-7
Link:

Abstract:
Dead variable reduction is a well-known optimization used to reduce state space. In this paper we present two novel reductions for explicit-state code model checking. These reductions are designed to efficiently handle multi-threaded heap-manipulating programs. We implemented the reductions in Java PathFinder and demonstrated their efficiency by verification of several non-trivial programs. We also formally show correctness of the approach.

BibTeX:
@inproceedings{jancik_dead_2016,
    title = {{Dead Variable Analysis for Multi-threaded Heap Manipulating Programs}},
    author = {Jančík, Pavel and Kofroň, Jan},
    year = {2016},
    booktitle = {{Proceedings of the 31st Annual ACM Symposium on Applied Computing}},
    publisher = {ACM},
    series = {{SAC '16}},
    location = {New York, NY, USA},
    doi = {10.1145/2851613.2851826},
    isbn = {978-1-4503-3739-7},
    pages = {1620--1627},
    url = {http://doi.acm.org/10.1145/2851613.2851826},
}