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:

	RADA-Java	RADA-SML
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.

Download

	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

Instruction

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.
Unzip the zip file.
Go to the folder containing rada.jar and rada_lib that you just unzipped.
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

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

Java version

Download

Instruction

Related Papers