Skip to main content.

Welcome to DIVINE Multi-Core!

The tool is based on automata-theoretic approach to LTL model checking. The input language allows for specification of processes in terms of extended finite automata and the verified system is then obtained as an asynchronous parallel composition of these processes. This system is in turn synchronously composed with a property process (negative claim automaton) obtained from the verified LTL formula through a Büchi automaton construction.

The resulting finite product automaton is then checked for presence of accepting cycles (fair cycles), indicating nonemptiness of its accepted language -- which in turn indicates invalidity of the verified LTL property.

Based on proven DiVinE LTL model checking system, DiVinE Multi-Core brings parallel verification to contemporary high-powered multi-core architectures. DiVinE Multi-Core exploits full power of modern x86 hardware and reduces unnecessary delays in workflow. Employing state-of-the-art parallel liveness checking algorithm, DiVinE Multi-Core offers unmatched scalability on shared memory platforms in the range of 2- to 16-core machines. Moreover, the tool supports 64-bit platforms out of the box, allowing it to leverage all the memory available in contemporary systems (and systems of the upcoming years).

In the current DiVinE Multi-Core release, input is provided in DVE format -- an industry-strength specification language, as used in original DiVinE, with plenty of diverse example models, ranging from simple toys to complex real-world models. An extensive model database is available at BEEM database.

Moreover, DiVinE can read models specified in ProMeLa (as used in the SPIN tool), in addition to its native DVE format. However, the capabilities of the tool on ProMeLa models is currently limited by inability to produce counterexamples: you can only obtain a yes/no answer.

DiVinE-MC Algortihm

The algorithm employed for accepting cycle detection is OWCTY augmented with a heuristic for on-the-fly cycle detection inspired by the MAP algorithm. It is not the purpose of this tool paper to go into details of the algorithm, so for in-depth description, we refer the reader to the two cited papers.

The main idea behind the OWCTY algorithm is to use topological sort for cycle detection -- an algorithm that does not depend on DFS postorder and can be thus parallelized reasonably well. Detection of cycles in this way is linear, but since we do accepting cycle detection, provisions for removing non-accepting cycles need to be added. This makes the algorithm quadratic in the worst case for general LTL properties, although for a significant subset of formulae (those that translate to weak Büchi automata) the algorithm runs in linear time in the size of the product automaton.

The MAP algorithm uses maximal accepting predecessors to identify accepting cycles in the product automaton. The main idea is based on the fact that each accepting vertex lying on an accepting cycle is its own predecessor. Instead of expensively computing and storing all accepting predecessors for each accepting vertex (which would be sufficient to conclude the presence of an accepting cycle), the algorithm computes only a single representative accepting predecessor for each vertex -- the maximal one in a suitable ordering. Clearly, if an accepting vertex is its own maximal accepting predecessor then it lies on an accepting cycle. This condition is used as the heuristic mentioned above. Note that the opposite direction does not hold in general. It can happen that the maximal accepting predecessor for an accepting vertex on a cycle does not lie on the cycle and the original MAP algorithm employs additional techniques to handle such a case.

If the heuristic fails, the OWCTY run will still detect accepting cycles if present. The heuristic does not interfere in any way when there are no accepting cycles -- OWCTY will detect that condition by itself. The cost of the heuristic is a very slight increase in per-state memory usage, and a small runtime penalty in the first phase of the first iteration of OWCTY. Overall, it does not increase the time complexity compared to OWCTY and in a number of cases it detects property violation without generating the entire state space, which makes the combined algorithm on-the-fly.

However, even though the algorithm is not asymptotically optimal, in practice it is hardly a problem when it comes to performance -- the bottlenecks can be found elsewhere.

Usage

Please refer to the Tool Guide for an overview of tool usage.

Download

The latest release of DiVinE Multi-Core and install instructions can be found on the download page.