[doc: New front page (with a few bits still missing). Petr Rockai **20220517212211 Ignore-this: 73c4fbb8e588941492671ed6d9cfaa2604ac4cbb5430c98e5578b2f96f22823c682cae726533107d ] hunk ./doc/web.home.txt 1 -DIVINE is a modern, explicit-state **model checker**. Based on the **LLVM** -toolchain, it can **verify programs** written in multiple real-world -programming languages, including **C** and **C++**. The verification core is -built on a foundation of **high­-per­for­mance algorithms** and data -structures, scaling all the way from a laptop to a high-end cluster. Learn -more in the [manual](manual.html). Our plans for upcoming releases are outlined -in the [roadmap] [rmap]. - -# DIVINE 4.2 Released - -[2019-01-15] A year since last major release, we are pleased to announce that -DIVINE version 4.2 has been released. Like all 4.x releases, the changes -included in 4.2 were integrated gradually. The 4.1.x series, culminating in the -release of 4.2 today has brought substantially improved POSIX compatibility, to -a level where packages like `gzip` or `coreutils` can be configured and -compiled using `divcc`, which creates binaries which can be verified in divine -and also executed in production. In this case, the executable binary code is -derived from the exact same bitcode that is processed by the model checker. - -Other highlights include much faster bitcode loading, improved support for -relaxed memory models used by Intel `x86_64`-series processors, support for C11 -threads, verification of synchronous systems specified using C with LTL -properties, much faster and more robust symbolic verification mode. Basic -support for detection of memory leaks has also been added, along with a large -number of smaller improvements and fixes detailed in the [release notes] -[rnotes]. - -Previously: [more news] [news]. - -# Use in Publications - -When you refer to DIVINE in an academic paper, we would appreciate if you could -use the following reference (our currently most up-to-date tool paper): +# synopsis + + divine verify program.c [program arguments] + +# description + +The ‹divine› toolset … + +# 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: +$$html old news. + +# see also + +$$html
+$$html valgrind(1), +$$html asan(7), +$$html klee(1), +$$html symbiotic(1), … +$$html
+ +# 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: hunk ./doc/web.home.txt 87 -# Contacting Us - -If you have comments or questions about DIVINE, please send an email to divine -at fi.muni.cz. - -[rmap]: roadmap.html -[rnotes]: whatsnew.html -[dl]: download.html -[news]: previously.html +# authors + +If you have comments or questions about ‹divine›, please send an email to +‹divine at fi.muni.cz›.