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 30 articles , 2 standard articles )

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

1 2 next

  1. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (2018)
  2. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  3. AlTurki, Musab A.; Meseguer, José: Executable rewriting logic semantics of Orc and formal analysis of Orc programs (2015)
  4. Martí-Oliet, Narciso; Ölveczky, Peter Csaba; Talcott, Carolyn: José Meseguer: scientist and friend extraordinaire (2015)
  5. Riesco, Adrián; Asavoae, Irina Mariuca; Asavoae, Mihail: Memory policy analysis for semantics specifications in Maude (2015)
  6. Colvin, Robert J.: An operational semantics for object-oriented concepts based on the class hierarchy (2014)
  7. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  8. 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)
  9. Meseguer, José: Twenty years of rewriting logic (2012)
  10. Lochbihler, Andreas; Bulwahn, Lukas: Animating the formalised semantics of a Java-like language (2011)
  11. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
  12. Roşu, Grigore; Şerbănuţă, Traian Florin: An overview of the K semantic framework (2010)
  13. Alba-Castro, M.; Alpuente, M.; Escobar, S.; Ojeda, P.; Romero, D.: A tool for automated certification of Java source code in Maude (2009) ioport
  14. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  15. Hills, Mark: Memory representations in rewriting logic semantics definitions (2009)
  16. Lescaylle, Alexei; Villanueva, Alicia: The \textsftccpinterpreter (2009)
  17. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
  18. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  19. Boichut, Yohan; Genet, Thomas; Jensen, Thomas; Le Roux, Luka: Rewriting approximations for fast prototyping of static analyzers (2007)
  20. 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)

1 2 next

Further publications can be found at: