Taclet Validation

In a project to validate the program transformation rules of KeY, Ralf Sasse has developed an extended lifted Maude Java semantics, which can be downloaded here. It is based on a prototypic semantics developed by Feng Chen at the University of Illinois at Urbana-Champaign. You can find information about this here. More information on the validation of KeY taclets using Maude can be found in the paper Automatic Validation of Transformation Rules for Java Verification against a Rewriting Semantics and Ralf Sasse's report Taclets vs. Rewriting Logic - Relating Semantics of Java.
Download extended lifted maude semantics.

Last modified: Mon Feb 19 11:53:45 CST 2007