@inbook{c6d2f6d4f68d4053b68cac46a12e3de2,
title = "Formal analysis of Java programs in JavaFAN",
abstract = "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.",
author = "Azadeh Farzan and Feng Chen and Jos{\'e} Meseguer and Grigore Ro{\c s}u",
note = "Copyright: Copyright 2020 Elsevier B.V., All rights reserved.",
year = "2004",
doi = "10.1007/978-3-540-27813-9_46",
language = "English (US)",
isbn = "3540223428",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "501--505",
editor = "Rajeev Alur and Peled, {Doron A.}",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "Germany",
}