Skip to content
A tool for automatic Montecarlo Arithmetic analysis.
C M4 Python C++ Shell Fortran Other
Branch: master
Clone or download
Pull request Compare This branch is 97 commits behind verificarlo:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.

verificarlo logo

Verificarlo v0.2.1

Build Status

A tool for automatic Montecarlo Arithmetic analysis.

Using Verificarlo through its Docker image

A docker image is available at This image uses the last git master version of Verificarlo and includes support for Fortran and uses llvm-3.5 and gcc-4.7.

Example of usage:

$ cat > test.c <<HERE
#include <stdio.h>
int main() {
  double a = 0;
  for (int i=0; i < 10000; i++) a += 0.1;
  printf("%0.17f\n", a);
  return 0;

$ docker pull verificarlo/verificarlo
$ docker run -v $PWD:/workdir verificarlo/verificarlo \
   verificarlo test.c -o test
$ docker run -v $PWD:/workdir verificarlo/verificarlo \
$ docker run -v $PWD:/workdir verificarlo/verificarlo \


Please ensure that Verificarlo's dependencies are installed on your system:

Then run the following command inside verificarlo directory:

   $ ./
   $ ./configure
   $ make
   $ sudo make install

If you do not care about Fortran support, you can avoid installing gfortran and dragonegg, by passing the option --without-dragonegg to configure:

   $ ./
   $ ./configure --without-dragonegg
   $ make
   $ sudo make install

If needed LLVM path, dragonegg path, and gcc path can be configured with the following options:

   $ ./configure --with-llvm=<path to llvm install directory> \
                 --with-dragonegg=<path to> \
                 CC=<gcc binary compatible with installed dragonegg>

Once installation is over, we recommend that you run the test suite to ensure verificarlo works as expected on your system:

   $ make installcheck

If you disable dragonegg support during configure, fortran_test will fail.

For example on an x86_64 Ubuntu 14.04 release, you should use the following install procedure:

   $ sudo apt-get install libmpfr-dev clang-3.3 llvm-3.3-dev dragonegg-4.7 \
       gcc-4.7 gfortran-4.7 autoconf automake build-essential

   $ cd verificarlo/
   $ ./
   $ ./configure \
       --with-dragonegg=/usr/lib/gcc/x86_64-linux-gnu/4.7/plugin/ \
   $ make 
   $ sudo make install
   $ make installcheck


To automatically instrument a program with Verificarlo you must compile it using the verificarlo command. First make sure that the verificarlo installation directory is in your PATH.

Then you can use the verificarlo command to compile your programs. Either modify your makefile to use verificarlo as the compiler (CC=verificarlo and FC=verificarlo ) and linker (LD=verificarlo) or use the verificarlo command directly:

   $ verificarlo *.c *.f90 -o ./program

If you only wish to instrument a specific function in your program, use the --function option:

   $ verificarlo *.c -o ./program --function=specificfunction

When invoked with the --verbose flag, verificarlo provides detailed output of the instrumentation process.

It is important to include the necessary link flags if you use extra libraries. For example, you should include -lm if you are linking against the math library and include -lstdc++ if you use functions in the standard C++ library.

MCA Configuration Parameters

Two environement variables control the Montecarlo Arithmetic parameters.

The environement variable VERIFICARLO_MCAMODE controls the arithmetic error mode. It accepts the following values:

  • MCA: (default mode) Montecarlo Arithmetic with inbound and outbound errors
  • IEEE: the program uses standard IEEE arithmetic, no errors are introduced
  • PB: Precision Bounding inbound errors only
  • RR: Random Rounding outbound errors only

The environement variable VERIFICARLO_PRECISION controls the virtual precision used for the floating point operations. It accepts an integer value that represents the virtual precision at which MCA operations are performed. Its default value is 53. For a more precise definition of the virtual precision, you can refer to

Verificarlo supports two MCA backends. The environement variable VERIFICARLO_BACKEND is used to select the backend. It can be set to QUAD or MPFR

The default backend, MPFR, uses the GNU multiple precision library to compute MCA operations. It is heavily based on mcalib MPFR backend.

Verificarlo offers an alternative MCA backend: the QUAD backend. QUAD backend uses the GCC quad types to compute MCA operations on doubles and the double type to compute MCA operations on floats. It is much faster than the MPFR backend, but is recent and still experimental.

One should note when using the QUAD backend, that the round operations during MCA computation always use round-to-zero mode.

In Random Round mode, the exact operations in given virtual precision are preserved.


The tests/ directory contains various examples of Verificarlo usage.


The postprocessing/ directory contains postprocessing tools to compute floating point accuracy information from a set of verificarlo generated outputs.

For now we only have a VTK postprocessing tool which takes multiple VTK outputs generated with verificarlo and generates a single VTK set of files that is enriched with accuracy information for each floating point DataArray.

For more information about, please use the online help:

$ postprocess/ --help

Unstable branch detection

It is possible to use Verificarlo to detect branches that are unstable due to numerical errors. To detect unstable branches we rely on llvm-cov coverage reports. To activate coverage mode in verificarlo, you should use the --coverage flag.

This is demonstrated in tests/test_unstable_branches/; the idea first introduced by verrou, is to compare coverage reports between multiple IEEE executions and multiple MCA executions.

Branches that are unstable only under MCA noise, are identified as numerically unstable.

Branch instrumentation

Verificarlo can instrument floating point comparison operations. By default, comparison operations are not instrumented and default backends do not make use of this feature. If your backend requires instrumenting floating point comparisons, you must call verificarlo with the --inst-fcmp flag.

How to cite Verificarlo

If you use Verificarlo in your research, please cite the following paper:

author    = {Christophe Denis and
             Pablo de Oliveira Castro and
             Eric Petit},
title     = {Verificarlo: Checking Floating Point Accuracy through Monte Carlo
booktitle = {23nd {IEEE} Symposium on Computer Arithmetic, {ARITH} 2016, Silicon
             Valley, CA, USA, July 10-13, 2016},
pages     = {55--62},
year      = {2016},
url       = {},
doi       = {10.1109/ARITH.2016.31},

A preprint is available at

Thanks !

Discussion Group

For questions, feedbacks or discussions about Verificarlo you can join our group at,!forum/verificarlo


Copyright (c) 2018 Universite de Versailles St-Quentin-en-Yvelines

Copyright (c) 2015 Universite de Versailles St-Quentin-en-Yvelines CMLA, Ecole Normale Superieure de Cachan

Verificarlo is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

Verificarlo is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with Verificarlo. If not, see

You can’t perform that action at this time.