Dead Variable Analysis for Multi-threaded Heap Manipulating Programs

Proceedings paper

Title:

Authors:

P. Jančík, J. Kofroň

Publication:

Proceedings of the 31st Annual ACM Symposium on Applied Computing

DOI:

10.1145/2851613.2851826

Year:

2016

ISBN:

978-1-4503-3739-7

Link:

http://doi.acm.org/10.1145/2851613.2851826

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},
}