Formal JVM Code Analysis in JavaFAN

JavaFAN uses a Maude rewriting logic specification of the JVM semantics as the basis of a software analysis tool with competitive performance. It supports formal analysis of concurrent JVM programs by means of symbolic simulation, breadth-first search, and LTL model checking. We discuss JavaFAN’s executable formal specification of the JVM, illustrate its formal analysis capabilities using several case studies, and compare its performance with similar Java analysis tools.

• Type: Conference
• Year: 2004
• Where: AMAST
• Authors: Azadeh Farzan, José Meseguer, Grigore Rosu
• Keywords: AMAST 2004, Analysis Tools, Concurrent Jvm Programs, Formal Analysis, Software Engineering