COmpiling Program
Semantics into TErm Rewriting
From a .class file obtained from the compilation of .java files (use
javac -target 1.5 to have .class files compatible with Copster),
Copster produces a Term Rewriting System (TRS) simulating the execution
of the Java program. Copster can export TRS in the Maude format and in the Timbuk format.
Download Copster version 1.0 (this
version uses Peano arithmetic) or 
Download CopsterLTA version 1.0 (this
version uses built-in integer arithmetic in Maude or Timbuk).
For instance, from this simple Java program,
CopsterLTA produces this TRS in Maude
or this one in Timbuk.
Online manual or pdf version.
Copster needs Ocaml
3.10 or later to be compiled. See the README
file for compilation instructions.
Copster: Copyright (C) 2009
Nicolas Barré, Laurent Hubert. Luka Le Roux and Thomas Genet
CopsterLTA: Copyright (C) 2012
Valérie Murat, Nicolas Barré, Laurent Hubert. Luka Le
Roux and Thomas Genet
Javalib: Copyright (C)
2005-2009, Etienne André, Frédéric Besson, Nicolas
Canasse, Laurent Hubert, Tiphaine Turpin
Supported by ANR-SETI RAVAJ.