Formal analysis of Java programs in JavaFAN

Azadeh Farzan, Feng Chen, José Meseguer, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingChapter

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsRajeev Alur, Doron A. Peled
PublisherSpringer-Verlag Berlin Heidelberg
Pages501-505
Number of pages5
ISBN (Print)3540223428, 9783540223429
DOIs
StatePublished - 2004

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3114
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formal analysis of Java programs in JavaFAN'. Together they form a unique fingerprint.

Cite this