synopsis
divine verify program.c [program arguments]
download
The most recent available release (as a source tarball) is
description
The
divine toolset (to be written)…
what's new
We are currently working on version 5, which will bring considerable internal
changes, support for LLVM 13+, streamlined build, and many improvements in
performance and reliability. The timeline is not yet finalized, but preview
releases are expected in 2022. Stay tuned.
Previously:
old news.
see also
history
The history of
divine dates back to circa 2000. In its initial
incarnation, it was an explicit-state distributed model checker with a
dedicated, non-embedded domain-specific language: think SPIN, but in
distributed memory (i.e. using resources of an entire compute cluster to
tackle larger problems than a single computer could handle). The name stood
for ‘distributed verification environment’ (it is not a coincidence that it
was created in paradise: a ‘parallel and distributed systems laboratory’).
By 2007, the focus was shifting towards shared-memory parallelism,
reflecting the trends in hardware development. In the following years, there
were brief detours into GPU-based acceleration to speed up computation and
into using external memories (hard drives, flash storage) to tackle state
spaces that would not fit into RAM of contemporary machines.
In 2011, generating state spaces of LLVM bitcode programs became our
dominant research direction. Even though distributed computation was still
supported at this time, it was clearly not a priority, and was entirely
removed by 2017 in the 4.0 release, along with support for half a dozen
input languages. Model checking of C and C++ programs, via LLVM, was very much
the main focus at this point. Verification of liveness properties, specified
using LTL, got likewise sidelined – it was first dropped early in the 4.x
series, though unlike support for distributed memory, limited LTL support was
soon re-introduced.
Around 2016, automatic abstraction bubbled up to the top of our priority
list, and has remained there since. Our method of choice was to implement
abstraction as an LLVM → LLVM program transformation, and by 2019, we had a
reasonably solid implementation. The semantics of abstract domains were
implemented in C++ and substituted into the program by LART (LLVM Abstraction
and Refinement Tool). Unfortunately, we have encountered a number of
‘impedance mismatches’ around LLVM, and both the discovery of instructions
that need to be substituted, as well as the substitution itself, turned out to
be fragile and complicated.
At the same time, a combination of factors (with the COVID-19 pandemic playing
a prominent role) essentially ground the development effort to a halt. At the
moment (spring 2022), we are slowly picking up the pieces and the pace to
chart a new course and restart development.
academic use
When you refer to
divine in an academic paper, we would appreciate if you
could use the following reference:
@InProceedings{BBK+17,
author = {Zuzana Baranová and Jiří Barnat and Katarína Kejstová and
Tadeáš Kučera and Henrich Lauko and Jan Mrázek and Petr Ročkai
and Vladimír Štill},
title = {Model Checking of {C} and {C}++ with {DIVINE} 4},
booktitle = {Automated Technology for Verification and Analysis},
pages = {201-207},
volume = 10482,
series = {LNCS},
year = 2017,
publisher = {Springer},
doi = {10.1007/978-3-319-68167-2_14}
}
authors
If you have comments or questions about
divine, please send an email to
divine at fi.muni.cz.