Authors: Henrich Lauko, Petr Ročkai, Jiří Barnat

Symbolic computation is an important approach in automated program analysis. Most state-of-the-art tools perform symbolic computation as interpreters and directly maintain symbolic data. In this paper, we show that it is feasible, and in fact practical, to use a compiler-based strategy instead. Using compiler tooling, we propose and implement a transformation which takes a standard program and outputs a program that performs semantically equivalent, but partially symbolic, computation. The transformed program maintains symbolic values internally and operates directly on them hence the program can be processed by a tool without support for symbolic manipulation.

The main motivation for the transformation is in symbolic verification, but there are many other possible use-cases, including test generation and concolic testing. Moreover using the transformation simplifies tools, since the symbolic computation is handled by the program directly. We have implemented the transformation at the level of LLVM bitcode. The paper includes an experimental evaluation, based on an explicit-state software model checker as a verification backend.



A source tarball of the version evaluated in the paper is available. For information on building and installing DIVINE from the tarball, please refer to the manual.

Alternatively, a prebuilt static binary for x84-64 Linux is available here: divine-4.1.5+2018.05.29.

Evaluation and Benchmarks

For evaluation, we have used the tools described in the following sections.

DIVINE + the transformation from the paper



For benchmarking, we have used a subset of the SV-COMP test cases, namely 7 categories, sumarized in the comparison section. We have only taken examples with finite state spaces since the simple approach outlined in the paper cannot handle infinite recursion or infinite accumulation loops. In total, we have selected 1160 SV-COMP inputs. The whole set of benchmarks is available from here:


The number of benchmarks correctly solved by each of the evaluated tools. The
best result in each category is rendered in boldface.

category total DIVINE* SymDIVINE CBMC
array 190 96 68 93
bitvector 32 17 9 2
loops 178 72 67 9
product-lines 575 336 411 234
pthread 45 9 0 1
recursion 81 47 43 22
systemc 59 14 27 0
total 1160 591 625 361

Time Comparison

We have compared benchmarks on which both tools have finished. Both axes in the plots are in seconds.

DIVINE compared to SymDIVINE:

DIVINE compared to CBMC:

State-space Comparison

We have only compared SymDIVINE and DIVINE regarding the size of state spaces, because CBMC does not build an explicit state space.