Author name cluster

Fabian Emmes

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

1 author row

LOPSTR Conference 2012 Conference Paper

Symbolic Evaluation Graphs and Term Rewriting - A General Methodology for Analyzing Logic Programs

Jürgen Giesl
Thomas Ströder
Peter Schneider-Kamp
Fabian Emmes
Carsten Fuhs

Abstract There exist many powerful techniques to analyze termination and complexity of term rewrite systems (TRSs). Our goal is to use these techniques for the analysis of other programming languages as well. For instance, approaches to prove termination of definite logic programs by a transformation to TRSs have been studied for decades. However, a challenge is to handle languages with more complex evaluation strategies (such as Prolog, where predicates like the cut influence the control flow). We present a general methodology for the analysis of such programs. Here, the logic program is first transformed into a symbolic evaluation graph which represents all possible evaluations in a finite way. Afterwards, different analyses can be performed on these graphs. In particular, one can generate TRSs from such graphs and apply existing tools for termination or complexity analysis of TRSs to infer information on the termination or complexity of the original logic program. More information can be found in the full paper [1].

Details

LOPSTR Conference 2011 Conference Paper

A Linear Operational Semantics for Termination and Complexity Analysis of ISO Prolog

Thomas Ströder
Fabian Emmes
Peter Schneider-Kamp
Jürgen Giesl
Carsten Fuhs

Abstract We present a new operational semantics for Prolog which covers all constructs in the corresponding ISO standard (including “non-logical” concepts like cuts, meta-programming, “all solution” predicates, dynamic predicates, and exception handling). In contrast to the classical operational semantics for logic programming, our semantics is linear and not based on search trees. This has the advantage that it is particularly suitable for automated program analyses such as termination and complexity analysis. We prove that our new semantics is equivalent to the ISO Prolog semantics, i. e. , it computes the same answer substitutions and the derivations in both semantics have essentially the same length.

Details

LPAR Conference 2008 Conference Paper

Improving Context-Sensitive Dependency Pairs

Beatriz Alarcón
Fabian Emmes
Carsten Fuhs
Jürgen Giesl
Raúl Gutiérrez
Salvador Lucas
Peter Schneider-Kamp
René Thiemann

Abstract Context-sensitive dependency pairs (CS-DPs) are currently the most powerful method for automated termination analysis of context-sensitive rewriting. However, compared to DPs for ordinary rewriting, CS-DPs suffer from two main drawbacks: (a) CS-DPs can be collapsing. This complicates the handling of CS-DPs and makes them less powerful in practice. (b) There does not exist a “ DP framework ” for CS-DPs which would allow one to apply them in a flexible and modular way. This paper solves drawback (a) by introducing a new definition of CS-DPs. With our definition, CS-DPs are always non-collapsing and thus, they can be handled like ordinary DPs. This allows us to solve drawback (b) as well, i. e. , we extend the existing DP framework for ordinary DPs to context-sensitive rewriting. We implemented our results in the tool AProVE and successfully evaluated them on a large collection of examples.

Details