Combining partial order reduction with symbolic model checking

(eng) Model checking is an efficient technique for verifying properties on asynchronous systems. Unfortunately, it suffers from the so-called combinatorial state-space explosion problem. Two common approaches are used to fight this problem, with different perspectives. On the one hand, partial-order reduction methods explore a reduced state space in a property-preserving way. On the other hand, symbolic techniques use efficient structures such as binary decision diagrams to concisely encode and compute large state spaces. This thesis presents algorithms which, one way or another, combine symbolic model checking and partial-order reduction, allowing efficient verification of CTL-X and LTL-X properties on models featuring asynchronous processes. At the root of our work was the ImProviso algorithm for computing reachable states, which combines POR and symbolic verification, and the FwdUntil method that supports verification of a subset of CTL. We present the PartialExploration algorithm which adapts and extends ImProviso to support the verification of a fragment of CTL-X. Then, the evalCTLX algorithm which merges the PartialExploration algorithm with the classical backward algorithm to support the totality of CTL.Afterwards, we extend our PartialExploration algorithm to checks LTL-X properties. The resulting algorithm is called evalCTLX. Thereafter, we present the BPE algorithm which adapts our PartialExploration algorithm and bounded model checking techniques to check LTL-X properties The algorithms developed in this thesis were implemented in the Milestones model checker. It allows us to check LTL properties, and CTL properties. Moreover, it can translate a model into an equivalent Spin model or NuSMV model.