JavaFAN

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.

Tool and Documentation

• Rewriting Logic Semantics of Java

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.
PDF, LNCS, CAV'04, DBLP, BIB