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

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

1 2 next

  1. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  2. Lochbihler, Andreas: Fast machine words in Isabelle/HOL (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. Bodin, Martin; Chargueraud, Arthur; Filaretti, Daniele; Gardner, Philippa; Maffeis, Sergio; Naudziuniene, Daiva; Schmitt, Alan; Smith, Gareth: A trusted mechanised JavaSript specification (2014)
  7. Colvin, Robert J.: An operational semantics for object-oriented concepts based on the class hierarchy (2014)
  8. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2013)
  9. Roşu, Grigore; Ştefánescu, Andrei; Ciobâca, Ştefan; Moore, Brandon M.: One-path reachability logic (2013)
  10. 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)
  11. Meseguer, José: Twenty years of rewriting logic (2012)
  12. Lochbihler, Andreas; Bulwahn, Lukas: Animating the formalised semantics of a Java-like language (2011)
  13. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project: a progress report (2011)
  14. Roşu, Grigore; Şerbănuţă, Traian Florin: An overview of the K semantic framework (2010)
  15. Alba-Castro, M.; Alpuente, M.; Escobar, S.; Ojeda, P.; Romero, D.: A tool for automated certification of Java source code in Maude (2009) ioport
  16. Boichut, Yohan; Héam, Pierre-Cyrille; Kouchnarenko, Olga: How to tackle integer weighted automata positivity (2009)
  17. Hills, Mark: Memory representations in rewriting logic semantics definitions (2009)
  18. Lescaylle, Alexei; Villanueva, Alicia: The \textsftccpinterpreter (2009)
  19. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
  20. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)

1 2 next

Further publications can be found at: