Formal Analysis of Java Programs in JavaFAN
A follow-up work of specifying Java semantics using rewriting logic is described in A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages.
- Formal Analysis of Java Programs in JavaFAN
- Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
- CAV'04, LNCS 3114, pp 501 - 505. 2004.
- Abstract. JavaFAN is a Java program analysis framework, that can symbolically execute multithreaded programs, detect safety violations searching through an unbounded state space, and verify finite state programs by explicit state model checking. Both Java language and JVM bytecode analyses are possible. JavaFAN's implementation consists of only 3,000 lines of Maude code, specifying formally the semantics of Java and JVM in rewriting logic and then using the capabilities of Maude for efficient execution, search and LTL model checking of rewriting theories.