Formal analysis of Java programs in JavaFAN

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 pro-grams 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. 1 JavaFAN’s Design JavaFAN (Java Formal ANalyzer) is a tool to simulate and formally analyze multithreaded Java programs at source code and/or bytecode levels. A novel feature of JavaFAN’s design is that it is directly based on formal definitions of the Java and JVM semantics in the form of rewrite theories that are efficiently executed and analyzed in the Maude language [1]. The following types of analysis are supported: (1) symbolic simulation, with Java and JVM specifications use