Dead Variable Analysis for Multi-Threaded Heap Manipulating Programs

Abstrakt

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.

Klíčová slova

• Dead variable analysis
• Dead variable reduction
• Static analysis
• State matching
• Explicit state model checking