Home

What is the goal of AProVE, and how does it work? The main idea behind AProVE and the research we are working on at the 'Programming Languages and Verification' chair at RWTH Aachen University is explained in the following short introductory video.

Quick Start Guide

Here you can find a quick guide that describes how to set up the AProVE development environment. Please follow the steps carefully to ensure a working configuration.

• Setting up the Environment

Learning the structure of AProVE

The following pages provides an overview of how AProVE works internally. Please read all of the pages carefully before working on new features to understand where and how to implement new stuff.

• Understanding AProVE: The Overall Structure
• Understanding AProVE: Problems
• Understanding AProVE: Processors
• Understanding AProVE: Proofs
• Understanding AProVE: Strategy Evaluation and 'the Machine'
• Understanding AProVE: SMT Solving
• Understanding AProVE: Languages
• Understanding AProVE: Project Layout
• Understanding AProVE: Ant build file
• Understanding AProVE: Sources of Nondeterminism in AProVE
• Understanding AProVE: Abortions and Timers
• Understanding AProVE: The Immutables Library

Using AProVE

• Using AProVE from the Command Line
• Using the AProVE Programmatic API
• Using the JSON Server
• Benchmarking
• Benchmark Worker (persistent JVM)

Coding Conventions and Tips for Development

Please have a look at the code conventions for AProVE before creating a pull request. You can also find some interesting tips and pitfalls you should avoid when working on AProVE.

• Code Conventions
• AProVE Utilities
• Hints and Pitfalls

Competitions where AProVE participates

• Termination Competition

  Content: termination and complexity analysis of programs written in Java, C, Haskell, Prolog, many variants of term rewrite systems, and many variants of integer transition systems.

  Benchmark Set: The competition runs on the termination problem database (TPDB).

• Confluence Competition

  Content: confluence, reachability, and related analysis of programs written in different variants of term rewrite systems.

  Benchmark Set: The competition runs on the ARI-COPS database (ARI-COPS).

• Software Verification Competition

  Content: termination, memory safety, reachability, and similar analysis of programs written in C.

  Benchmark Set: The competitions runs on the termination problem database (SV-Benchmarks).

Miscellaneous

• The Theorem Prover Hidden Within AProVE