Automated Termination Analysis of Java Bytecode by Term Rewriting
From MaRDI portal
Publication:5389149
DOI10.4230/LIPIcs.RTA.2010.259zbMath1236.68145OpenAlexW2124765047MaRDI QIDQ5389149
Jürgen Giesl, Marc Brockschmidt, Carsten Otto, Christian von Essen
Publication date: 25 April 2012
Full work available at URL: http://subs.emis.de/LIPIcs/frontdoor_f283.html
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Grammars and rewriting systems (68Q42)
Related Items
Verifying Procedural Programs via Constrained Rewriting Induction ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Lower-bound synthesis using loop specialization and Max-SMT ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ A framework for computing finite SLD trees ⋮ Termination Graphs for Java Bytecode ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs
Uses Software