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

SML version

The version of CVC4 that RADA-SML is currently compatible with is CVC4-2011-12-16. We are working on making RADA support the newest version of CVC4 with some help from the CVC4 team.

January 2013: We decided to rewrite RADA in Java. Visit this page for more information.

Download Last update
RADA-SML report Oct 12, 2012
Source code Oct 23, 2012
Benchmarks Oct 19, 2012
Intermediate smt2 files Oct 19, 2012

Experimental Results

Related Papers

  1. The Guardol Language and Verification System. [pdf]
    David Hardin, Konrad Slind, Michael Whalen, and Tuan-Hung Pham. TACAS'12.
  2. Satisfiability Modulo Recursive Programs. [pdf]
    Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak. SAS'11.