Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

DOI10.4230/LIPIcs.RTA.2011.155zbMath1236.68036OpenAlexW2160568515MaRDI QIDQ5389079

Marc Brockschmidt, Jürgen Giesl, Carsten Otto

Publication date: 24 April 2012

Full work available at URL: http://subs.emis.de/LIPIcs/frontdoor_3df8.html

zbMATH Keywords

recursionterminationterm rewritingJava bytecode

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Analyzing program termination and complexity automatically with \textsf{AProVE}, Automatically proving termination and memory safety for programs with pointer arithmetic, From Jinja bytecode to term rewriting: a complexity reflecting transformation, A framework for computing finite SLD trees

Uses Software

• AProVE