^       —————.   —.—  .     .  —.—  .     .  .—————    .    .
   ———      |     |   |   |     |   |   ||    |  |         |    |
  —(o)—     |     |   |   |     |   |   |  |  |  |————     '————|
 ———————    |     |   |    |   |    |   |    ||  |              |
—————————   —————'   —'—     '     —'—  '     '  '—————         '

DIVINE 4.3

• In 4.3.0 (2019-06-01):
  • DiOS configurations are now static, and selected with --dios-config.
  • The system call sequence in DiOS no longer relies on indirect calls.
  • DiOS can now be loaded into KLEE, in addition to DIVINE.
  • Numerous fixes in dataflow value propagation in LART.
  • Improved ABI compatibility of DiOS with the host platform.
  • Better coverage of POSIX APIs (header files) in DiOS.
  • Add support for linking C++ programs to divcc.

DIVINE 4.2

• In 4.2.7 (2019-05-01):
  • Portability improvements (should build & work on OpenBSD again).
  • Initial support for string abstraction based on the M-String domain.
  • A number of fixes in LART abstraction passes.
  • Reduce the memory used for globals (ballooned due to a change in LLVM).
  • Minor improvements in usability of sim.
  • Fix a regression which caused divine draw to be unusable.
  • Restore support for reading global variables in sim (via $globals).
  • Minor improvements in support for relaxed memory models.
• In 4.2.5 (2019-04-01):
  • Initial support for aggregate abstract domains.
  • Simplified passing of abstract arguments and return values.
  • Prepare ground for interval-based tracking of user metadata.
• In 4.2.4 (2019-03-15):
  • Rewrite the concurrent hash table used in the model checker.
  • Implement a fast, low-overhead hash function (based on a custom design).
• In 4.2.2 (2019-02-15): TBD
• In 4.2.1 (2019-02-02): TBD
• In 4.2.0 (2019-01-15): TBD

DIVINE 4.1

• In 4.1.21 (2019-01-01):
  • __vm_clone now takes a second argument (objects blocked from clone).
  • Fix a number of memory leaks in DiOS.
  • Fix lowering of llvm.fabs.* intrinsics.
  • A number of libc compatibility improvements.
• In 4.1.20 (2018-12-15):
  • The DiOS kernel and libc now build with -fno-exceptions.
  • Reduce the size and improve linking granularity of DiOS.
  • Link the DiOS kernel at load time, not at bitcode link time.
  • The passthrough mode in DiOS has been disabled until further notice.
  • Clean up and unify memory management in the DiOS kernel.
  • Import lld and use it as the linker in divcc.
  • Improve --leakcheck return by doing the check after, not before, ret.
  • Improve handling of memory instructions in LART abstraction passes.
  • Add support for the -l flag to divcc.
  • Add support for divcc -pthread.
  • Add support for (discrete) clock simulation to DiOS.
  • A number of improvements to the M-String abstract domain.
  • Improve ABI and API compatibility of DiOS with the host system.
• In 4.1.19 (2018-12-01):
  • An initial implementation of the M-String abstract domain.
  • Small improvements in DiOS’ compatibility with glibc.
  • Make the memory management in the VM slightly more flexible.
  • Improve the control register API in DiVM.
  • Allow liveness properties to be provided as HOA-formatted TGBAs.
  • Add a lightweight LTL formula simplifier to divine ltlc.
• In 4.1.18 (2018-11-15):
  • Add a --leakcheck option to divine verify (and check).
  • Simplify checks for uninitialised mutexes in DiOS pthreads.
  • Refactor the DiOS VFS and make it build with -fno-exceptions.
  • Add support for a ‘star’ (unit) domain to LART and DiOS.
  • Initial support for floating-point arithmetic in LART abstraction.
  • Do not rely on RTTI in the DiOS kernel.
  • Substantially improve the robustness of linking in divcc.
  • Simplify abstract domain descriptions employed by LART.
  • Refactor the abstraction passes in LART.
• In 4.1.11 - 4.1.17: Minor changes only.
• In 4.1.8 (2018-06-01):
  • Show the SMT formulas for path condition in counterexample traces.
• In 4.1.7 (2018-06-01):
  • Import a large number of SV-COMP test cases.
  • Substantial expansion of POSIX compatibility in DiOS.
  • Add an --svcomp option for dealing with SV-COMP quirks.
  • A number of fixes in the abstraction engine in LART.
  • Fix a few problems in the weakmem runtime support code.
• In 4.1.6 (2018-05-15):
  • Track pointers through bitshift operations.
  • Improve the efficiency of pointer encoding.
  • Import STP and CryptoMiniSat into the source tree.
  • Add support for STP as the SMT backend and make it the default.
  • Robustness improvements in the VM.
  • Substantial improvements in divbench (and some in divcheck).
  • Improve compatibility and usability of divcc.
  • Rewrite the LART abstraction pass to leverage dynamic tainting.
  • Make implementation of new abstract domains easier.
  • Cover a number of missing cases in abstract value propagation.
  • Add a very simple SMT query cache.
• In 4.1.5 (2018-05-01):
  • Add __vm_peek and __vm_poke hypercalls.
  • Robustness improvements and bugfixes in pointer and heap-related code.
  • Fix instrumentation of control-flow loop detection.
  • Testsuite improvements.
• In 4.1.4 (2018-04-15):
  • Improved coverage of pthread and C11 thread APIs.
  • Do not rely on the OS to mark certain memory objects as shared.
  • The divcc compiler now also works with cmake-based projects.
• In 4.1.3 (2018-04-01):
  • Produce counterexamples for violations of liveness properties.
  • A new, more flexible implementation of shadow memory.
  • Basic support for C11 thread APIs.
  • Simpler and more efficient support for relaxed memory models.
  • A more robust implementation of the dbg.call instruction.
• In 4.1.2 (2018-03-15):
  • Support for dynamic tainting in DiVM.
  • Allow verification of bitcode embedded in ELF binaries.
  • Track and re-assemble byte-sized pointer fragments.
• In 4.1.1 (2018-03-12):
  • Display an instructions-per-second figure when running interactively.
  • Use a more compact frame representation / make bitcast a noop.
  • Support linking to Z3.
  • Much more efficient exploration strategy in symbolic mode.
  • Better interaction of data non-determinism with tau reduction.
  • Revamped and extended functional test suite.
  • Improved performance of shadow memory.
  • Improved coverage of POSIX APIs in DiOS.
  • Better binary compatibility of DiOS libc with glibc.
  • Many improvements in divbench.
  • Build system improvements.
  • Replace divine run with exec & use syscall passthrough by default.
  • A fair scheduler is now available in DiOS.
  • Better support for x86-TSO, removed support for other memory models.
  • Portable (i.e. not Linux-specific) syscall passthrough.
  • Replace the __vm_control hypercall with a simpler __vm_ctl_* set.
  • Replace the __vm_interrupt_* hypercalls with __vm_test_*.
  • A reworked, simpler syscall mechanism in DiOS.
  • New command for comparing objects in the simulator (diff).
  • The verify, check &c. commands now recognize a --synchronous flag.
  • Low-level support for memory leak detection.
• In 4.1.0 (2018-01-15):
  • Do not leak transient objects.
  • Improved support for building static Linux binaries.
  • Track per-bit value definedness.

DIVINE 4.0

• In 4.0.22 (2018-01-01):
  • Add an info command to sim.
  • Make fast-forwarding in sim more configurable & useful.
  • Improve compatibility of libc headers with glibc.
• In 4.0.21 (2017-12-15):
  • Fix a use-after-free and an out-of-bounds access in DiVM.
  • Avoid crashes after failures in dbg.call.
  • A number of improvements in the user interface.
  • Make it possible to build real static binaries.
• In 4.0.20 (2017-12-01):
  • Preliminary support for SV-COMP ‘built-in’ functions (__VERIFIER_*).
  • Fix a crash in divine draw.
  • Make it possible to build DIVINE with g++.
• In 4.0.19 (2017-11-15):
  • Implement a synchronous scheduler in DiOS.
  • Allow DIVINE to be built using a (C++17-compatible) system toolchain.
  • Implement abstraction of global variables.
  • Improve efficiency of the relaxed memory verification mode.
  • Enforce permissions in access to the flags control register.
• In 4.0.18 (2017-11-01):
  • Improvements in handling of abstract (symbolic) structures.
  • Allow abstraction of aggregate return types.
• In 4.0.16 (2017-10-01):
  • Recognize command prefixes (e.g. ch for check) in command parsers.
  • Another batch of symbolic verification improvements.
  • Add a call command to sim.
• In 4.0.15 (2017-09-15): Further relax τ reduction.
• In 4.0.14 (2017-09-01):
  • Experimental support for relaxed memory models (--relaxed-memory).
  • Introduce a divine check subcommand (less strict than verify).
  • Improve τ reduction substantially & fix a regression.
  • Implement an init file to execute commands at sim startup.
  • Allow sim to spawn auxilliary X terminals.
  • Automatically write report files with detailed verification output.
  • Use a much more robust counter-example format.
  • Add a dbg.call instruction to improve VM efficiency.
  • Make DiOS VFS work with multi-processes programs.
  • Fix a possible infinite loop due to inadequate CFL interrupt tracking.
  • Use human-friedly thread IDs in trace output.
  • More improvements in symbolic verification.
  • Implement setup --pygmentize for colourful source in sim.
• In 4.0.13 (2017-08-15):
  • A number of improvements in symbolic verification.
  • Reduce memory requirements of sim.
  • Make type names of DiOS components human-readable.
• In 4.0.12 (2017-07-15):
  • Implement assorted process-related syscalls.
  • Add pthread_atfork to the threading library.
• In 4.0.11 (2017-07-01):
  • Add a --trace option to divine run to trace instructions.
  • Preliminary implementation of divcc, a drop-in compiler replacement.
• In 4.0.10 (2017-06-15):
  • Preliminary support for syscall passthrough in divine run.
  • Initial implementation of the fork system call.
• In 4.0.8 (2017-05-15):
  • Improved precision of memory access tracking in τ reduction.
  • Update the bundled libc++abi and libc++ to version 4.0.0.
• In 4.0.6 (2017-04-15):
  • A rudimentary version of verify --liveness.
  • The DiOS kernel has been separated into reusable components.
• In 4.0.5 (2017-04-01): Make standard IO unbuffered by default to save memory.
• In 4.0.4 (2017-03-15):
  • Improved POSIX signal handling in DiOS.
  • Cleaner layout of runtime headers (libc/dios/divm).
  • Fix a build error when the system compiler is clang 4.
• In 4.0.3 (2017-03-01):
  • An improved and much faster implementation of C++ exceptions.
  • Improved verification speed and smaller memory footprint.
• In 4.0.2 (2017-02-15):
  • Improved bitcode linker, libraries as .a archives.
  • Detailed, SQL-based reporting and logging.
  • Inclusion of a (semi-)automated benchmarking tool, ‘divbench’.
  • Update pdclib to the current upstream (2017-01-18).
  • Numerous improvements in symbolic verification support.
  • Faster verification of thread-less programs with --sequential.
  • An important bugfix in treatment of memory access in tau reduction.
  • A more efficient runtime representation of the bitcode.
  • Intrinsic lowering is now handled in LART.
• In 4.0.1 (2017-01-15):
  • Support weak pointers that do not count towards state comparison.
  • A new __vm_syscall hypercall for accessing the host OS.
  • Make the objid hint a VM control register, _VM_SC_ObjIdShuffle.
  • Experimental support for verify --symbolic (needs Z3).
  • Extended memory use statistics when --report yaml-long is specified.
  • Experimental support for run -o syscall:passthrough.
  • A complete libm implementation is now bundled with divine cc.
  • Support for regex.h has been added to divine cc.
  • Preliminary support for user-provided program monitoring functions.
• In 4.0.0 (2017-01-09):
  • Improved compatibility of text output with YAML.
  • make prerequisites installs dependencies on common distributions.

DIVINE 3.90

• Substantial rewrite with focus on software verification.
• More flexible and cohesive interface between the program and the VM.
• Includes DiOS, a small operating system kernel and standard C/C++ libraries.
• More comprehensive runtime environment (provided by DiOS).
• An interactive debugger/simulator and a counterexample viewer (divine sim).

LIMITATIONS: This is a beta version. Additionally, verification of LTL (liveness) properties and distributed verification are not currently available and are planned for a later version in the 4.x series. Only C and C++ models are supported at this time: DVE, DESS, CESMI, UPPAAL and other input formalisms are not supported, but may become available in later versions.

DIVINE 3.x

3.3

• [3.3.1] Implement –fair (weak fairness) for LLVM.
• [3.3.1] Substantial improvements in tree compression.
• [3.3.1] Much faster (ca. 50%) LLVM interpreter.
• [3.3.1] Fix support for –probabilistic LLVM.
• [3.3.1] Fix LTL in C++ source files.
• [3.3.1] Add subtyping support to C++ catch clauses.
• [3.3.1] Improved DESS (explicit state space) support.
• [3.3.1] Fix –fair support (weak fairness, affects DVE and LLVM).
• [3.3.2] Make gen-explicit work with –shared.
• [3.3.2] Use –shared by default for parallel verification.
• [3.3.2] Fix several bugs in combination of –shared with –compression.
• [3.3.2] Make builds with assertions significantly faster.
• [3.3.2] Support for –fair is now built in by default.
• [3.3.2] Fix export of DESS files larger than 2GB.
• [3.3.3] Fix broken counterexamples with –fair.
• [3.3.3] Enable simulate with –fair for LLVM.

3.2

• [3.2.2] Fix bug #301 (assertion failure when -p not given).
• [3.2.3] Support for storing boolean state properties in DESS.
• [3.2.3] Fix broken MPI support.
• [3.2.4] Fix linking of TBB malloc or HOARD (when enabled).
• [3.2.4] Fix races in pdclib stdio code.
• [3.2.4] Implement machine-readable statistics output.
• [3.2.4] Multiple fixes to libc (pdclib) functionality.
• [3.2.4] Fix backward compatibility with DESS files exported from divine < 3.2.3.

3.2.1

• LLVM: The divine compile subcommand no longer uses ld.gold.
• LLVM: Add fine-grained options in --property specification.
• LLVM: Allow verification of points-to LLVM metadata.
• LLVM: Programs that use stringstreams can now be verified.
• LLVM: Implement stacksave and stackrestore intrinsics.
• LLVM: Many optimisations.
• timed: Implement ultraregion automatons in the UPPAAL generator.
• timed: Verification of untimed LTL with clock constraints.
• Improved CLI simulator interface.
• Implement context-switch-directed reachability.
• Improved reporting of verification results.
• Many, many bugfixes and internal code improvements.

3.0.92 (3.1 beta 1; 6.1.2014)

• LLVM: Make “problem” reports more informative.
• LLVM: Make std::thread work, albeit inefficiently.
• LLVM: Add a low-level interface to report custom errors.
• LLVM: Detect dereferences of out-of-scope local variables.
• LLVM: Detect memory leaks.
• LLVM: Detect branches conditional on uninitialised values.
• LLVM: Implement realloc, atexit (in user-space).
• LLVM: Report unhandled (C++) exceptions.
• LLVM: Fix an alignment bug in global aggregate initialisers.
• LLVM: Run global constructors before main().
• Fix win32 builds.
• Improve the CLI simulator.
• Add a --simulate-counterexample option to verify.
• Allow multiple reports (text + sql) for a single run.
• Significantly improved build efficiency (time and memory).
• Various bugfixes and minor enhancements.

DIVINE 3.0.91 (3.1 alpha 2; 27.10.2013)

• Implement --shared support in OWCTY and MAP (liveness checking).
• Support creation of persistent, explicit graph dumps (.dess).
• Support for exception handling in C++ w/ LLVM.
• Optional probabilistic choice with LLVM.
• Support for std::atomic in C++ verification w/ LLVM.
• LLVM support for cmpxchg, atomicrmw instructions.
• Fix for a bug in tau reduction for LLVM (bad load coalescing).
• Varargs support in C, C++ w/ LLVM.
• Optionally demangle C++ symbols in counterexamples.
• Port and use libc++ and libc++abi in divine compile --llvm.
• divine compile --llvm now #defines __divine__.
• Reduced memory requirements for compilation.
• Support for UPPAAL nested structures, arrays and meta variables.
• Implement conditional instantiation in DVE.
• The verification report can be now stored using SQL/ODBC.

3.0.90 (3.1 alpha 1; 14.7.2013)

• Improved shared-memory verification of safety properties.
• Substantially improved memory efficiency.
• Optional lossless tree-based state-space compression.
• Support for C++ standard library in divine compile --llvm.
• Improvements to the DVE specification language.
• Extensive internal code refactorings.
• More efficient memory allocation code.

3.0 (13.7.2013)

• Fix a bug in loading LTL properties in the LLVM backend.
• Fix handling of property processes in the DVE compiler.
• Add support for LLVM 3.3.
• Fix a couple issues in divine compile --llvm.
• Updates to the manual.

DIVINE 2.x

2.97 (3.0 RC 2 ; 21.5.2013)

• Fix layout issues with LLVM bitcode files using a 64b pointer layout.
• Fix a problem where unresolved symbols in LLVM bitcode would be silently ignored, and treated as nulls.
• The above also prompted a number of changes and improvements in divine compile --llvm, which now provides a nearly complete ISO C library implementation, as well as a C++ ABI support library.
• Let the LLVM interpreter detect & report double frees and divisions by zero.

2.96 (3.0 RC 1 ; 17.4.2013)

• A bug in the parallel C3 proviso has been found and fixed.
• Zeno-run elimination in timed automata (use --fairness to enable).
• Re-enable external-memory (disk) queues.
• Improvements in DVE parsing and error reporting.
• Broken/unused algorithms have been removed (compact, probabilistic).
• Multiple-unit support for divine compile --llvm.
• Substantial improvements in --shared support (still experimental though).
• Many bugfixes and minor improvements.

2.95 (3.0 beta 2 ; 16.3.2013)

• Support pthread barriers in the LLVM runtime.
• Improvements in the LTL support for divine compile --cesmi.
• Fix statistics tracking in models with > 2^31 states.
• MURPHI compiler now works with current CESMI.
• The correctenss bug in MAP is now fixed (divine verify --map).
• New POR C1+C2 implementation for DVE.
• LLVM backend now supports aggregate registers.
• Reduce startup overhead for LLVM & DVE and improve cache sharing.
• Many bugfixes.

2.94 (3.0 beta 1 ; 13.2.2013)

• Substantial updates to the CESMI interface (see manual).
• Re-introduce the DVE->CESMI compiler (divine compile file.dve).
• A new interactive subcommand, divine simulate.
• Updates and improvements to timed automata support.
• A number of bugfixes.

2.93 (3.0 alpha 3 ; 28.1.2013)

• New implementation of resource limits (–max-memory, –max-time) which circumvents the previous 2G limit and also works on Windows.
• divine compile --cesmi now works on Windows as well.
• Builds with LLVM 3.1 and 3.2.
• Many bugfixes.

2.92 (3.0 alpha 2 ; 21.1.2013)

• Implement detection of time deadlocks in timed automata verification.
• An overhauled, more flexible CESMI interface & documentation.
• Implement a new approach to CESMI + LTL in divine compile --cesmi.
• New CLI interface and accompanying documentation (manpage, manual section).
• Enable all applicable reductions by default (--no-reduce to disable).
• Re-enable LTL properties for LLVM bitcode.
• Consistently support models with multiple initial states.
• Many bugfixes.

2.91 (3.0 alpha 1; 7.1.2013)

• LLVM backend for model checking of C/C++ programs.
• A new DVE language interpreter.
• Support for (weak) fairness restrictions.
• Support for verification of models based on timed automata, using the Uppaal modelling language and arbitrary untimed LTL formulas.
• Hash compaction (optional): conserve memory in exchange for a small possibility of missing a counterexample.
• Allow spilling of long queues on disk to free memory for hash tables.
• Run verification in-process in the GUI.
• divine compile –llvm: Call clang to compile a C or C++ program using a special implementation of “pthreads” library, producing LLVM bitcode suitable for verification with divine.
• divine compile –cesmi: Conveniently build C and C++ modules for the divine CESMI loader.
• Use Intel ThreadBuildingBlocks memory allocator by default (HOARD can still be activated at configure time).
• Improved Windows support.
• Many bugfixes and minor improvements.

2.5.2 (4.12.2011)

• Fix compatibility with GCC 4.6.
• Make compilation work also on openmpi installations without ompi/version.h.
• Fix installation of the GUI.

2.5.1 (5.4.2011)

• DVE compiler fixes: initial state in some models could be incorrect in compiled DVE. When the system was in deadlock and LTL property had been present, the resulting model could overwrite origin states, causing the model checker to misbehave. Both these problems are fixed in this release.

2.5 (28.2.2011)

• A faster hash table implementation.
• A new tool, “divine draw”, for state space visualisation (using graphviz).
• More compact state representation in the DVE compiler.
• Fix a bug in MAP where self-loops could be missed.
• Support for a new input language, CoIN, available with all algorithms.
• Fix a couple of bugs in the DVE compiler. The binary models could cause infinite loops in DiVinE or lead to incorrect state spaces.
• Add support for “divine combine” on Windows.
• A new option, –gnuplot-statistics, for machine-readable queue size stats.

2.4 (29.9.2010)

• C3 check for parallel partial order reduction.
• Partial order reduction for (interpreted) DVE (–por).
• Real-time hashtable & queue statistics (–statistics).
• Custom generators are not allowed with pool-less builds.
• Further optimisations to the exploration engine (hash table, FIFOs, MPI).
• Better –version output.
• In addition to G++, DiVinE can be compiled with Clang now.
• More fixes in MPI.
• A curses-based interface for observing runtime algorithm behaviour.
• Dual-threaded nested DFS (Holzmann ’07).
• Counterexamples in (single-threaded) nested DFS.
• Enable on-the-fly heuristic in distributed (MPI) OWCTY.
• Make “divine verify” work with non-DVE inputs correctly.
• Fix BA translation of F((F a) U b) form formulae (J. Strejcek &c.)

2.3 (8.8.2010)

• Basic support for Murphi model compilation and parallel verification.
• Fix a bug in DVE compiler that made some models uncompilable.
• Improved, distributed (MPI-enabled) MAP algorithm.
• Track state space statistics in OWCTY (–report).
• Proper deadlock detection (with traces) for all model types.
• Improved –report output format consistency.
• Fix handling of committed states in the DVE compiler.
• Multiple stability and correctness fixes in distributed memory support (MPI).
• Limit the override of global allocator to avoid occasional crashes in glibc.
• Add an option to limit maximum verification runtime (–max-time, POSIX only).

Furthermore, a new binary ABI is available in this release. There are two caveats though:

1. The ABI is NOT STABLE and should not be relied upon. It will be subject of further changes in future releases.

2. The win32 support is somewhat limited, since some models may expect access to symbols exported by the divine binary itself, which is not supported on win32.

2.2 (17.2.2010)

• Further optimisations in compiled DVE.
• Improved overall performance of the verifier.
• “divine combine” can be used again (it’s been broken in previous releases)
• Compiled models can now be loaded on Windows.
• New option, -i (–initial-table) to set intial hashtable size. This can be used to further improve performance, assuming knowledge of model size.

An overall speed improvement of 20 - 30 % may be expected for dual-core reachability and LTL verification when using compiled DVE, over version 2.1.1. Please note that dve.so files generated by this version are not compatible with DiVinE 2.1.1.

KNOWN ISSUES: Error state handling is not consistent between interpreted and compiled DVE. The profiled build (-DPROFILE=ON) is currently broken. (Both issues exist since version 2.1.)

2.1.1 (26.1.2010)

• Fixed a number of issues with compiled DVE models.
• Bugfixes in the custom model loader.
• Improved performance of compiled DVE.
• Fixed Windows build.

2.1 (17.1.2010)

• A new DVE to C (to native binary) compiler available as `divine compile’.
• Fixed handling of error states in interpreted DVE.
• The GUI can now be compiled & used on Windows.
• A number of GUI improvements and usability fixes.

2.0 (19.11.2009)

• This version is a major rewrite of the parallel framework and algorithms.
• MPI is now partially supported in addition to shared memory parallelism OpenMPI 1.3 is recommended.
• A new graphical user interface is available, including model editor, simulator and a counterexample browser.
• Support for running on Windows (win32) machines (shared memory only).
• It is now possible to load models in form of ELF shared objects (POSIX only).
• More data available in –report (including machine-readable counterexample).
• The divine.combine binary has been removed, use “divine combine” instead.

DiVinE Multi-Core

1.4 (23.4.2009)

• Unfortunately, an incorrect implementation of Nested DFS has slipped into the 1.3 release. Version 1.4 fixes this problem.
• Early counterexample discovery in OWCTY has been improved: accepting self-loops are now detected on-the-fly, and early termination is now more efficient.

1.3 (17.11.2008)

• Improved and newly included algorithms:
  • MAP: improved progress reports, early termination and counterexamples
  • Nested DFS for single-threaded verification (no counterexamples)
• A new “verify” subcommand to run the most suitable algorithm for given input and number of cores (currently does not produce counterexamples when used with -w 1 due to the abovementioned Nested DFS limitation).
• Counterexample generation in OWCTY has suffered from a bug that prevented it from finishing in any reasonable time on some property/model combinations. This has been fixed.
• A few other user experience fixes: improved warnings and overall robustness.

1.2.1 (1.11.2008)

• Fix compilation with g++ 4.3.
• Update the bundled version of HOARD to 3.7.1.
• Include some updates to the bundled version of wibble (no major impact on DiVinE itself).

1.2 (15.5.2008)

• A few minor bugfixes.
• The divine-mc.combine utility can now handle .mdve and .mprobdve files.
• Parallel shared-memory probabilistic model checker ProbDiVinE-MC has been added to the distribution, built as divine-mc.probabilistic.
• NIPS interpreter updated to version 1.2.8

1.1

• The OWCTY algorithm now performs an on-the-fly heuristic to speed up discovery of counterexample.
• Added divine-mc.combine to the distribution.
• Added report generation functionality (-r commandline switch) to facilitate mass experimental runs.
• New commandline switch –max-memory to limit address space available to the tool. Can be used to avoid swapping.
• Counterexample generation can now be disabled through –no-counterexample commandline switch.
• A dummy high-speed state space generator for performance analysis. It is used when no input file is given.
• A prototype ProMeLa state space generator and an accompanying bytecode compiler. ProMeLa models can be verified, although no counterexample generation is implemented.
• Developer documentation updates.

1.0

Initial release.