Modular termination proofs of recursive Java bytecode programs by term rewriting
DOI10.4230/LIPICS.RTA.2011.155zbMATH Open1236.68036OpenAlexW2160568515MaRDI QIDQ5389079FDOQ5389079
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
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cited In (9)
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- A framework for computing finite SLD trees
- From Jinja bytecode to term rewriting: a complexity reflecting transformation
- Termination graphs for Java bytecode
- Proving termination of programs automatically with AProVE
- Automated termination analysis of Java bytecode by term rewriting
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proving Termination of C Programs with Lists
- Complexity analysis for \textbf{Java} with \textsf{AProVE}
Uses Software
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)
