Difference between revisions of "JavaFAN"

From FSL
Jump to: navigation, search
Line 11: Line 11:
 
* Installation Instructions
 
* Installation Instructions
 
* User Manual
 
* User Manual
 +
* [[Rewriting Logic Semantics of Java]]
  
 
== Related Papers ==
 
== Related Papers ==
 
<purge></purge>
 
<purge></purge>
 
<pub noedit id='farzan-chen-meseguer-rosu-2004-cav'> </pub>
 
<pub noedit id='farzan-chen-meseguer-rosu-2004-cav'> </pub>

Revision as of 23:12, 8 December 2014

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)

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

Personal tools
Namespaces

Variants
Actions
Navigation