Formal analysis of Java programs in JavaFAN. 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.

References in zbMATH (referenced in 20 articles , 2 standard articles )

Showing results 1 to 20 of 20.
Sorted by year (citations)

  1. AlTurki, Musab A.; Meseguer, José: Executable rewriting logic semantics of Orc and formal analysis of Orc programs (2015)
  2. Colvin, Robert J.: An operational semantics for object-oriented concepts based on the class hierarchy (2014)
  3. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  4. Bae, Kyungmin; Ölveczky, Peter Csaba; Feng, Thomas Huining; Lee, Edward A.; Tripakis, Stavros: Verifying hierarchical Ptolemy II discrete-event models using real-time maude (2012)
  5. Meseguer, José: Twenty years of rewriting logic (2012)
  6. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
  7. Roşu, Grigore; Şerbănuţă, Traian Florin: An overview of the K semantic framework (2010)
  8. Alba-Castro, M.; Alpuente, M.; Escobar, S.; Ojeda, P.; Romero, D.: A tool for automated certification of Java source code in Maude (2009)
  9. Hills, Mark: Memory representations in rewriting logic semantics definitions (2009)
  10. Lescaylle, Alexei; Villanueva, Alicia: The \ssftccp interpreter (2009)
  11. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
  12. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  13. Boichut, Yohan; Genet, Thomas; Jensen, Thomas; Le Roux, Luka: Rewriting approximations for fast prototyping of static analyzers (2007)
  14. Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martí-Oliet, Narciso; Meseguer, José; Talcott, Carolyn: All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM. (2007)
  15. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project (2007)
  16. Ahrendt, Wolfgang; Roth, Andreas; Sasse, Ralf: Automatic validation of transformation rules for Java verification against a rewriting semantics (2005)
  17. Farzan, Azadeh; Chen, Feng; Meseguer, José; Roşu, Grigore: Formal analysis of Java programs in JavaFAN (2004)
  18. Farzan, Azadeh; Meseguer, José; Roşu, Grigore: Formal JVM code analysis in JavaFAN (2004)
  19. Meseguer, José; Braga, Christiano: Modular rewriting semantics of programming languages (2004)
  20. Meseguer, José; Roşu, Grigore: Rewriting logic semantics: from language specifications to formal analysis tools (2004)

Further publications can be found at: