Difference between revisions of "JavaFAN"

From FSL
Jump to: navigation, search
Line 3: Line 3:
== Rewriting Logic Semantics ==
== Rewriting Logic Semantics ==
* [[Rewriting Logic Semantics of Java]] -- Try the rewriting-based Java interpreter [http://fsl.cs.uiuc.edu/javafan/javarl-demo.html online!]
* [[Rewriting Logic Semantics of Java]]  
* [[Rewriting Logic Semantics of Java Bytecode]]
* [[Rewriting Logic Semantics of Java Bytecode]]

Revision as of 22:21, 15 November 2006

JavaFAN, standing for Java Formal ANalysis, is a rewrite logic based approach to formal definitions of the Java language and formal analysis of Java programs. In JavaFAN, we define executable rewrite logic semantics of both Java and Java Bytecode using Maude, which are not only formal semantic specifications but also interpreters to run Java programs on the source code level and/or on the bytecode level. Using the underlying search and model checking features of Maude, JavaFAN can be used to formally analyze Java programs without extra effort and has effectively been applied on a number of examples. More details can be found in our papers.

Rewriting Logic Semantics

Tool and Documentation (coming soon)

  • Download JavaFAN
  • Installation Instructions
  • User Manual

Related Papers

Formal Analysis of Java Programs in JavaFAN 
Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.

Personal tools