Sciweavers

AMAST
2004
Springer

Formal JVM Code Analysis in JavaFAN

14 years 4 months ago
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.
Azadeh Farzan, José Meseguer, Grigore Rosu
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where AMAST
Authors Azadeh Farzan, José Meseguer, Grigore Rosu
Comments (0)