Modular termination proofs of recursive Java bytecode programs by term rewriting

DOI10.4230/LIPICS.RTA.2011.155MaRDI QIDQ5389079zbMATH OpenOpenAlexFDO

Authors Marc Brockschmidt, Carsten Otto, Jürgen Giesl

Publication date 24 April 2012

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

zbMATH Keywords

Java bytecoderecursionterm rewritingtermination

Mathematics Subject Classification ID

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

Recommendations

• Automated termination analysis of Java bytecode by term rewriting
• Termination graphs for Java bytecode
• Proving termination of programs automatically with AProVE
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automated termination proofs for logic programs by term rewriting

Cited in

(9)

• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• A framework for computing finite SLD trees
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Termination graphs for Java bytecode
• Proving termination of programs automatically with AProVE
• Complexity analysis for \textbf{Java} with \textsf{AProVE}
• Automated termination analysis of Java bytecode by term rewriting
• Proving Termination of C Programs with Lists

Describes a project that uses

Uses Software

• AProVE

This page was built for publication: Modular termination proofs of recursive Java bytecode programs by term rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5389079)