Frontend vs. Backend Language? What's the difference?

AProVE is able to analyze termination and complexity of different programming languages. Here, we clearly distinguish between two types of languages: frontend languages and backend languages.

Frontend Language

Frontend languages are the programming languages that users write their software in. AProVE can handle programs written in C, Haskell, Prolog and Java by symbolically representing a given program P in a finite graph, called the symbolic execution graph. This graph overapproximates all possible runs of the program P. It builds this graph 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. Afterwards, AProVE transforms this symbolic execution graph into a backend language that is then analysed for termination and runtime complexity.

Backend Language

Backend languages are analysis-oriented representations designed specifically for automated reasoning. They capture only the essential behavior needed for formal analysis without any syntactic sugar. Examples include term rewrite systems or integer transition systems. These backend languages are not meant for programming by humans, but for enabling powerful, reusable algorithms that prove properties such as termination and complexity.

Advantages

By separating analysis of programs into the analysis of frontend languages and backend languages, we have multiple advantages:

Frontend Features Only Once: Language-specific features from different frontend languages have to be taken into account only once during the generation of the symbolic execution graph. The precise termination techniques can ignore such complex features that would make the analysis drastically more complex.

Backend Analysis is for Everyone: The same backend language can be used for several different frontend languages. Developing a new technique to analyse termination of a backend language does not only improve the state-of-the-art of the analysis of this specific language, but it improves all analysis that use the specific backend language.

Full Modularity: If you are just interested in part of the analysis procedure, you can use the different parts on their own. AProVE can export the generated symbolic execution graphs in the JSON format, which is both human-readable as well as suitable for automated processing. Moreover, AProVE can export the generated rewrite system (i.e., the program written in the backend language) as well.

The power of the mentioned modularity can be seen when one exports the symbolic execution graph into integer transition systems. Here, we can use dedicated tools for termination and complexity analysis like KoAT and LoAT. We can use their results to, e.g., infer upper and lower runtime bounds for the initially provided program written in C.

If you are interested in further information regarding the different parts of AProVE or the generation of the symbolic execution graph for each frontend language, then have a look at the reference section.

— The AProVE Team