UnderstandingAprove
This page provides a high-level overview of how AProVE works.
AProVE is built around problem classes and processor classes. The core workflow involves defining a problem and applying processors that transform a problem into different (simpler) ones or that directly yield results (e.g., a termination status or an upper complexity bound). We illustrate this idea in the following with a high-level example and a low-level example.
Let's walk through a simplified example where we aim to prove the termination of an algorithm implemented in Java.
-
Parse the Java Code: The first step is to parse the Java files and collect essential information about the program, such as variables, control flow, and an approximated execution graph. This information is encapsulated in a JAVA Problem object, which stores all the relevant details. Such a problem is a Java class that extends the
DefaultBasicObligationclass. -
Apply Processors: The JAVA Problem is passed through a series of processors. A processor is a Java class that implements the
Processorinterface. Each processor transforms the problem into another class or directly provides a result (such as 'YES' for termination or 'NO' for non-termination). -
Transformation Flow: Initially, we apply a processor to convert the JAVA Problem into a TRS Problem. We then apply additional processors on the TRS Problem. The final result will be a termination status, such as 'YES' or 'NO', or if no further processor is applicable, but we have not yet found a termination status result 'MAYBE'.
This general approach applies to all the different languages supported by AProVE. For more information about supported languages and how to integrate new languages into AProVE, see Understanding Languages.
Let’s explore how AProVE handles termination proofs for Term rewriting systems (TRS), which is implemented in the aprove.verification.dpframework.TRSProblem package. This package consists of three main sub-packages:
- Processors: Contains all the processors classes working on TRSProblems.
- Solvers: Includes wrappers for SAT or SMT solvers to deal with TRSProblems or specific solvers that can directly handle certain problems that arise when analyzing TRSProblems.
- Utility: Provides helper functions used across the package.
In the main package, there are multiple Problem classes. Each class represents a specific type of problem in the proof process. During a termination proof, you typically transform between different problem classes. For instance, you may start with a TRSProblem and later convert it into a QTRSProblem. Each problem type has its own dedicated class, with attributes and methods tailored to that specific problem. For more information about problems and how to implement them, see Understanding Problems. Additionally, Proof classes are used to customize the proof process, primarily to generate valid proof certificates and to visualize the complete proof to be humanly readable. If you are unfamiliar with proof certificates, these classes simply have an 'export()' function that prints the corresponding proof step as a string. For more information about proofs, see Understanding Proofs.
Processors are responsible for transforming problems into new forms that are typically smaller or easier to analyze. Mathematically speaking, a processor $ P $ takes a problem $ S $ and transforms it into a set of new problems
The Solvers package contains various solvers that AProVE uses to find solutions to specific problems. This includes general solvers, like SMT solvers, as well as solvers tailored to particular problems. More details on solvers and how to integrate them can be found in Understanding Solvers.
Finally, the Utility package houses all general helper functions that are required across the package but don't belong to any specific problem-, processor-, or solver class.