Zur Hauptnavigation / To main navigation

Zur Sekundärnavigation / To secondary navigation

Zum Inhalt dieser Seite / To the content of this page

Sekundärnavigation / Secondary navigation

Inhaltsbereich / Content

AADD: Affine Arithmetic Decision Diagrams

This page gives a brief introduction into AADD and provides downloads for the implementation of the AADD class library. An in-depth introduction of AADD can be found here

What are AADD?

Affine Arithmetic Decision Diagrams (AADD) are a model that allows us the efficient representation and tracing of uncertainties in mixed discrete/continuous computations. Examples are algorithms with "continuous" arithmetic computations and "discrete" control flow. An AADD consists of a binary decision diagram that represents the discrete uncertain decisions, and Affine Arithmetic Forms (AAF) at the leaf nodes, that represent continuous uncertain values.

A particular use case of AADD is symbolic execution or symbolic simulation. Symbolic execution of a software with some "uncertain" inputs allows us to increase verification coverage, or to do error injection simulation. If AADD are used in a simulator, they can also be used to trace the propagation of uncertainties through dynamical systems. 

  • For symbolic execution of a C++ program, replace variables of "double" or "int" data type with "AADD" abstract data type.
  • For symbolic simulation (for a given simulator), replace the value type of signals with AADD. 

Implementation

An implementation of AADD, together with some examples and all other packages needed can be downloaded below (single file with all packages). It consists of the following software packages, each in a separate folder or archive:

  • AADD with the implementation of Affine Arithmetic Forms. It includes an implementation of Affine Arithmetic Forms originally from EPFL, with improvements from Leibnitz Univ. Hannover, Vienna University of Technology, and University of Kaiserslautern. 
  • GLPK with a copy of the GLPK solver that is used in AADD to minimise over-approximation. 
  • SystemC that we use to demonstrate symbolic simulation based on AADD.
  • SystemC AMS that we use to demonstrate symbolic simulation based on AADD. 
  • Some examples. 

Installation

Installation is described in the file README. Basically, you have to install all required packages, set environment variables to its installation directory, and then to use cmake to build and install the AADD package and the examples. 

 

 

Downloads