RADA: A Tool for Reasoning about Algebraic Data Types with Abstractions

Java version

RADA is an open source and highly portable tool to reason about algebraic data types. The reasoning is based on creating an abstraction of the data type via a catamorphism (fold) function. The syntax for reasoning problems is presented as an extension of the SMT-Lib 2.0 format, supporting integration with tools that use this format. RADA uses a catamorphism unrolling algorithm and currently supports CVC4 and Z3 as underlying reasoning engines.

This page presents a new version of RADA, which was completely rewritten from scratch using Java and ANTLR 4. If you are looking for the SML version of RADA, please visit this page. Some main differences between the new RADA and RADA-SML are:

Syntax of datatype declarations (declare-datatypes () (...)) (declare-datatypes (...))
Syntax of testers is-X is_X

As of December 2013, RADA has been tested with the latest versions of CVC4 (version 1.3) and Z3 (version 4.3.0). Its source code was compiled using Java 1.7.

Prerequisite tools: CVC4, Z3, Java 1.7.


Last update
RADA FSE Tools Demo Video August 22, 2013
Binary file October 08, 2013
Source code (as an Eclipse archive file) October 08, 2013
Benchmark examples for FSE paper June 03, 2013
Benchmark examples for parameterized catamorphisms Aug 07, 2013


  1. Download the zip file via the link to "Binary file" above. The zip file contains rada.jar and rada_lib, a folder that consists of third-party libraries that RADA depends on.
  2. Unzip the zip file.
  3. Go to the folder containing rada.jar and rada_lib that you just unzipped.
  4. Run RADA as follows:

           java -jar rada.jar --solver solver_name [--showTempFiles] [--verbose #arg] file_path

    where solver_name is the name of the SMT solver in your system (cvc4 or z3) and file_path is the path to the input file. Note that the solver must be in your system path.

    Example: Assuming that you are in the folder containing rada.jar and rada_lib and you want to check the satisfiability of sumtree01.rada, one of our benchmark examples, with cvc4. The command you could use is as follows:

           java -jar rada.jar --solver cvc4 your_path_to_sumtree01/sumtree01.rada

Related Papers

  1. RADA: A Tool for Reasoning about Algebraic Data Types with Abstractions.
    Tuan-Hung Pham and Michael W. Whalen. ESEC/FSE'13.
  2. An Improved Unrolling-Based Decision Procedure for Algebraic Data Types. [pdf]
    Tuan-Hung Pham and Michael W. Whalen. VSTTE'13.
  3. The Guardol Language and Verification System. [pdf]
    David Hardin, Konrad Slind, Michael W. Whalen, and Tuan-Hung Pham. TACAS'12.
  4. Satisfiability Modulo Recursive Programs. [pdf]
    Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak. SAS'11.