Skip to content

Home

Jump to bottom
Christoph Matheja edited this page Mar 21, 2018 · 29 revisions

Contents

Quickstart

Documentation

People and Publications

What is Attestor?

Attestor is a verification tool that attempts to achieve both of these goals. To this aim, it first constructs an abstract state space of the input program by means of symbolic execution. Each state depicts both links between heap objects and values of program variables using a graph representation. Abstraction is performed on state level by means of graph grammars. They specify the data structures maintained by the program, and describe how to summarise substructures of the heap in order to obtain a finite representation. After labelling each state with propositions that provide information about structural properties such as reachability or heap shapes, the actual verification task is performed in a second step. To this aim, the abstract state space is checked against a user-defined LTL specification. In case of violations, a counterexample is provided.

System Requirements

The following software has to be installed prior to the installation of Attestor:

Reproducing Benchmarks

 (Unix-based operating systems)
 $ git clone https://github.com/moves-rwth/attestor-examples.git
 $ chmod +x run.sh
 $ ./run.sh
 
 (All operating systems)
 $ git clone https://github.com/moves-rwth/attestor-examples.git
 $ mvn clean install exec:exec@run

Given the system requirements, no installation of Attestor is required to reproduce and comprehend previously reported benchmark results. We collect all benchmarks in a separate repository including auxiliary scripts to install, run and evaluate all benchmarks. Please confer the documentation in the benchmark repository for further details.

Installation

$ git clone https://github.com/moves-rwth/attestor.git
$ mvn install

Please note that the installation requires an internet connection as maven will install additional dependencies.

Getting Started

After installation, an executable jar file is created in the directory target within the cloned repository. The name of executable jar is of the form

 attestor-<VERSION>-jar-with-dependencies.jar

where <VERSION> is the previously cloned version of the Attestor repository. To execute Attestor, it suffices to run

 $ java -jar attestor-<VERSION>-jar-with-dependencies.jar

from within the target directory. This should display a help page explaining all available command line options. Since the above jar file contains all dependencies, it is safe to rename it and move the file to a more convenient directory.

Detailed step-by-step instructions on using Attestor to analyze Java programs are found on the detailed walkthrough page.

Furthermore, we maintain a collection of running examples (including source code, user-defined graph grammars, and configuration files) in a separate repository. All of these examples can be directly executed using provided auxiliary scripts. Please confer the documentation in the examples repository for further details.

People

Attestor is developed at the Chair for Software Modeling and Verification at RWTH Aachen University by

Publications

Clone this wiki locally