Duet is a static analysis tool designed for analyzing concurrent programs.
Duet depends on several software packages. The following dependencies need to be installed manually.
On Ubuntu, you can install these packages (except Java) with:
sudo apt-get install opam libgmp-dev libmpfr-dev libntl-dev default-jre
On MacOS, you can install these packages (except Java) with:
brew install opam gmp mpfr
Next, add the sv-opam OPAM repository, and install the rest of duet's dependencies. These are built from source, so grab a coffee — this may take a long time.
opam remote add sv git://github.com/zkincaid/sv-opam.git opam install ocamlgraph batteries cil oasis ppx_deriving Z3 apron ounit menhir OCRS ntl
After Duet's dependencies are installed, it can be built as follows:
Duet's makefile has the following targets:
make: Build duet
make ark: Build the ark library and test suite
make apak: Build the apak library and test suite
make doc: Build documentation
make test: Run test suite
There are three main program analyses implemented in Duet:
- Data flow graphs:
duet.native -coarsen FILE
- Proof spaces:
duet.native -proofspace FILE
- Compositional recurrence analysis:
duet.native -cra FILE
Duet supports two file types (and guesses which to use by file extension): C programs (.c), Boolean programs (.bp).
By default, Duet checks user-defined assertions, which are specified by the built-in function
__VERIFIER_assert. Alternatively, it can also instrument assertions as follows:
duet.native -check-array-bounds -check-null-deref -coarsen FILE
Data flow graphs
-coarsen flag implements an invariant generation procedure for multi-threaded programs with an unbounded number of threads. The analysis is described in
- Azadeh Farzan and Zachary Kincaid: Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control. POPL 2012.
-proofspace flag implements a software model checking procedure for multi-threaded programs with an unbounded number of threads. The procedure is described in
- Azadeh Farzan, Zachary Kincaid, Andreas Podelski: Proof Spaces for Unbounded Parallelism. POPL 2015.
Compositional recurrence analysis
-cra flags an invariant generation procedure for sequential programs. The analysis is described in
- Azadeh Farzan and Zachary Kincaid: Compositional Recurrence Analysis. FMCAD 2015.
- Zachary Kincaid, John Cyphert, Jason Breck, Thomas Reps: Non-Linear Reasoning For Invariant Synthesis. POPL 2018.
Typically, it is best to run CRA with
-cra-split-loops. By default, the
-cra runs the analysis as described in POPL'18. The FMCAD'15 analysis can be run by setting the
The interprocedural variant is described in
- Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas Reps: Compositional Recurrence Analysis Revisited. PLDI 2017.
is available in the Newton-ark2 branch of this repository. Build instructions to come.
Duet is split into several packages:
Algebraic program analysis kit. This is a collection of utilities for implementing program analyzers. It contains various graph algorithms (e.g., fixpoint computation, path expression algorithms) and utilities for constructing algebraic structures.
Arithmetic reasoning kit. This is a high-level interface over Z3 and Apron. Most of the work of compositional recurrence analysis lives in ark.
Predicate automata library.
Implements program analyses, frontends, and anything programming-language specific.