AProVE analyzes programs by symbolically simulating all possible ways they can run. It builds a graph representing these behaviors while taking into account language-specific features of these frontend languages, such as memory handling in C, heap usage in Java, or lazy evaluation in Haskell. This graph is then translated into a backend language, e.g., term rewriting or integer transition systems, which AProVE uses to analyze termination and complexity. In case of integer transition systems, we rely on dedicated tools for termination and complexity analysis like KoAT and LoAT.
Click on the graph below to view the publications related to the part you selected.