Publication list

The inherent computational complexity of validating and verifying concurrent systems implies a need to be able to exploit parallel and distributed computing architectures. We present a new distributed algorithm for state space exploration of concurrent systems on computing clusters. Our algorithm relies on Remote Direct Memory Access (RDMA) for low-latency transfer of states between computing elements, and on state reconstruction trees for compact representation of states on the computing elements themselves. For the distribution of states between computing elements, we propose a concept of state stealing. We have implemented our proposed algorithm using the OpenSHMEM API for RDMA and experimentally evaluated it on the Grid'5000 testbed with a set of benchmark models. The experimental results show that our algorithm scales well with the number of available computing elements, and that our state stealing mechanism generally provides a balanced workload distribution.

The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order prescribed by the sweep-line method.

We describe a dynamic partitioning scheme usable by explicit state space exploration techniques that divide the state space into partitions, such as many external memory and distributed model checking algorithms. The goal of the scheme is to reduce the number of transitions that link states belonging to different partitions, and thereby limit the amount of disk access and network communication. We report on several experiments made with our verification platform ASAP that implements the dynamic partitioning scheme proposed in this paper. The experiments demonstrate the importance of exploiting locality to reduce cross transitions and IO operations, and using informed heuristics when choosing components to be used as a basis for partition refinement. The experiments furthermore show that the proposed approach improves on earlier techniques and significantly outperforms these when provided with access to the same amount of bounded RAM.

Partial order reduction limits the state explosion problem that arises in model checking by limiting the exploration of redundant interleavings. A state space search algorithm based on this principle may ignore some interleavings by delaying the execution of some actions provided that an equivalent interleaving is explored. However, if one does not choose postponed actions carefully, some of these may be infinitely delayed. This pathological situation is commonly referred to as the ignoring problem. The prevention of this phenomenon is not mandatory if one wants to verify if the system halts but it must be resolved for more elaborate properties like, for example, safety or liveness properties. We present in this work some solutions to this problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented in the Spin tool.

State caching is a memory reduction technique used by model checkers to alleviate the state explosion problem. It has traditionally been coupled with a depth-first search to ensure termination. We propose and experimentally evaluate an extension of the state caching method for general state exploring algorithms that are independent of the search order (i.e., search algorithms that partition the state space into closed (visited) states, open (to visit) states and unmet states).

The ComBack method is a memory reduction technique for explicit state space search algorithms. It enhances hash compaction with state reconstruction to resolve hash conflicts on-the-fly thereby ensuring full coverage of the state space. In this paper we provide two means to lower the run-time penalty induced by state reconstructions: a set of strategies to implement the caching method proposed in [20], and an extension through delayed duplicate detection that allows to group reconstructions together to save redundant work.

Model checking often requires the combined use of multiple reduction techniques to mitigate the state explosion problem. The contribution of this paper is a generalised sweep-line algorithm that enforces the conditions necessary for partial-order reduction in the form of stubborn sets to preserve LTL_-X properties. The core idea in our algorithm is to compute strongly connected components and detect cycles within each state space layer explored by the sweep-line method, while leveraging persistent states as anchor states for enforcing cross-layer partial-order reduction conditions. We have implemented our new algorithm and conducted an experimental evaluation on set of benchmarks from the Petri Nets Model Checking Contest. The results show our LTL_-X preserving combination of sweep-line exploration with partial-order reduction even in a conservative implementation may substantially reduce peak memory usage. Furthermore, the overhead is mostly similar to plain partial-order preserving LTL_-X reduction.

The implementation of model checking algorithms on real life systems usually suffers from the well known state explosion problem. Partial order reduction addresses this issue in the context of asynchronous systems. We review in this article algorithms developped by the Petri nets community and contribute with simple heuristics and variations of these. We also report on a large set of experiments performed on the models of a Model Checking Contest hosted by the Petri Nets conference since 2011. Our study targets the verification of deadlock freeness and liveness properties.

The inherent computational complexity of validating and verifying concurrent systems implies a need to be able to exploit parallel and distributed computing architectures. We present a new distributed algorithm for state space exploration of concurrent systems on computing clusters. Our algorithm relies on Remote Direct Memory Access (RDMA) for low-latency transfer of states between computing elements, and on state reconstruction trees for compact representation of states on the computing elements themselves. For the distribution of states between computing elements, we propose a concept of state stealing. We have implemented our proposed algorithm using the OpenSHMEM API for RDMA and experimentally evaluated it on the Grid'5000 testbed with a set of benchmark models. The experimental results show that our algorithm scales well with the number of available computing elements, and that our state stealing mechanism generally provides a balanced workload distribution.

We propose a distributed implementation of the collapse compression technique used by explicit state model checkers to reduce memory usage. This adapatation makes use of lock-free distributed hash tables based on one-sided communication primitives provided by libraries such as OpenSHMEM. We implemented this technique in the distributed version of the model checker Helena. We report on experiments performed on the Grid'5000 cluster with an implementation over OpenMPI. These reveal that, for some models, this distributed implementation can altogether preserve the memory reduction provided by collapse compression and reduce execution times by allowing the exchanges of compressed states between processes.

This article introduces a parallel state space exploration algorithm for shared memory multi-core architectures using state compression and state reconstruction to reduce memory consumption. The algorithm proceeds in rounds each consisting of three phases: concurrent expansion of open states, concurrent reduction of potentially new states, and concurrent duplicate detection. An important feature of the algorithm is that it requires little inter-thread synchronisation making it highly scalable. This is confirmed by an experimental evaluation that demonstrates good speed up at a low overhead in workload and with little waiting time caused by synchronisation.

This paper presents CNDFS, a tight integration of two earlier multi-core nested depth-first search (NDFS) algorithms for LTL model checking. CNDFS combines the different strengths and avoids some weaknesses of its predecessors. We compare CNDFS to an earlier ad-hoc combination of those two algorithms and show several benefits: It has shorter and simpler code and a simpler correctness proof. It exhibits more stable performance and scalability, while at the same time reducing memory requirements.

The algorithm has been implemented in the multi-core backend of the LTSmin model checker, which is now benchmarked for the first time on a 48 core machine (previously 16). The experiments demonstrate better scalability than other parallel LTL model checking algorithms, but we also investigate apparent bottlenecks. Finally, we noticed that the multi-core NDFS algorithms produce shorter counterexamples, surprisingly often shorter than their BFS-based counterparts.

The sweep-line method is an explicit-state model checking technique that uses a notion of progress to delete states from internal memory during state space exploration and thereby reduce peak memory usage. The sweep-line algorithm relies on the use of a priority queue where the progress value assigned to a state determines the priority of the state. In earlier implementations of the sweep-line method the progress priority queue is kept in internal memory together with the current layer of states being explored. In this paper we investigate a scheme where the current layer is stored in internal memory while the priority queue is stored in external memory. From the perspective of the sweep-line method, we show that this combination can yield a significant reduction in peak memory usage compared to a pure internal memory implementation. On an average of 60 example instances, this combination reduced peak memory usage by a factor of 25 at the cost of an increase in execution time by a factor of 2.5. From the perspective of external memory state space exploration, we demonstrate experimentally that the state deletion performed by the sweep-line method may reduce the I/O overhead induced by duplicate detection compared to a pure external memory state space exploration method.

The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least progress-first search order that prohibits the immediate use of standard on-the-fly LTL model checking algorithms that rely on a depth-first search order. This paper proposes and experimentally evaluates an algorithm for LTL model checking compatible with the search order prescribed by the sweep-line method.

We describe a dynamic partitioning scheme usable by model checking techniques that divide the state space into partitions, such as most external memory and distributed model checking algorithms. The goal of the scheme is to reduce the number of transitions that link states belonging to different partitions, and thereby limit the amount of disk access and network communication. We report on several experiments made with our verification platform ASAP that implements the dynamic partitioning scheme proposed in this paper.

The ignoring problem refers to the fact that some actions may be infinitely postponed by a state space search algorithm that makes use of partial order reduction (POR). The prevention of this phenomenon is mandatory if one wants to verify more elaborate properties than the deadlock freeness, e.g., safety or liveness properties. We present in this work some solutions to this problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented in the Spin tool.

The limited amount of memory is the major bottleneck in model checking tools based on an explicit states enumeration. In this context, techniques allowing an efficient representation of the states are precious. We present in this paper a novel approach which enables to store the state space in a compact way. Though it belongs to the family of explicit storage methods, we qualify it as semi-explicit since all states are not explicitly represented in the state space. Our experiments report a memory reduction ratio up to 95time in the worst case.

In this paper, we develop a syntactical version of elaborated reductions for high-level Petri nets. These reductions simplify the model by merging some sequential transitions into an atomic one. Their conditions combine local structural ones (e.g. related to the actions of a thread) and global algebraic ones (e.g. related to the threads synchronization). We show that these conditions are performed in a syntactical way, when a syntax of the color mappings is given. We show also how our method outperforms previous ones on a recent case study with regard both to the reduction ratio and the automatization of their application.

This paper presents the high level Petri nets analyzer Helena. Helena can be used for the on-the-fly verification of state properties, i.e., properties that must hold in all the reachable states of the system, and deadlock freeness. Some features of Helena make it particularly efficient in terms of memory management. Structural abstractions techniques, mainly transitions agglomerations, are used to tackle the state explosion problem. Benchmarks are presented which compare our tool to Maria. Helena is developed in portable Ada and is freely available under the conditions of the GNU General Public License.