Improved State Space Reductions for LTL Model Checking of C & C++ Programs

March 3, 2020

In this paper, we present substantial improvements in efficiency of explicit-state LTL model checking of C & C++ programs, building on [2], including improvements to state representation and to state space reduction techniques. The improved state representation allows to easily exploit symmetries in heap configurations of the program, especially in programs with interleaved heap allocations. Finally, we present a major improvement through a semi-dynamic proviso for partial-order reduction, based on eager local searches constrained through control-flow loop detection.

This work has been partially supported by the Czech Science Foundation grant No. GAP202/11/0312.

Authors: Petr RočkaiJiří Barnat, and Luboš Brim

Project: DIVINE4

Published in: NASA Formal Methods (NFM 2013), Springer, 2013, volume 7871 of LNCS, 1–15.

Go to pdf

Article Link


Partner University



Associated Research Projects