swMATH ID: 1934
Software Authors: Farzan, Azadeh; Chen, Feng; Meseguer, José; Roşu, Grigore
Description: Formal analysis of Java programs in JavaFAN. 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.
Homepage: http://fsl.cs.illinois.edu/index.php/JavaFAN
Related Software: Maude; K Prover; MMT; Java+ITP; ACL2; CafeOBJ; Isabelle/HOL; PMaude; Dist-Orc; Centaur; MOMENT2; OBJ3; ITP; Coq; JML; KOOL; K tool; Ptolemy; ITP/OCL; Stratego
Cited in: 30 Documents
Further Publications: http://fsl.cs.illinois.edu/index.php/FSL_Publications

Citations by Year