Formal analysis of Java programs in JavaFAN. (English) Zbl 1103.68611

Alur, Rajeev (ed.) et al., Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22342-8/pbk). Lecture Notes in Computer Science 3114, 501-505 (2004).
Summary: 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.
For the entire collection see [Zbl 1056.68003].


68Q60 Specification and verification (program logics, model checking, etc.)
68N99 Theory of software
Full Text: DOI