@inbook{483aeebe2a394c5fba1aa695075972be,
title = "Formal JVM code analysis in javaFAN",
abstract = "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.",
author = "Azadeh Farzan and Jos{\'e} Meseguer and Grigore Ro{\c s}u",
year = "2004",
doi = "10.1007/978-3-540-27815-3_14",
language = "English (US)",
isbn = "3540223819",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "132--147",
editor = "Charles Rattray and Savitri Maharaj and Carron Shankland",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}