JavaFAN

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

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

1 2 next

  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. Alba-Castro, Mauricio; Alpuente, María; Escobar, Santiago; Ojeda, Pedro; Romero, Daniel: A tool for automated certification of Java source code in maude (2009)
  10. Alpuente, María; Romero, Daniel: A visual technique for web pages comparison (2009)
  11. Hills, Mark: Memory representations in rewriting logic semantics definitions (2009)
  12. Hills, Mark: Memory representations in rewriting logic semantics definitions (2009)
  13. Lescaylle, Alexei; Villanueva, Alicia: The \ssftccp interpreter (2009)
  14. Lescaylle, Alexei; Villanueva, Alicia: The tccp interpreter (2009)
  15. Şerbănuţă, Traian Florin; Roşu, Grigore; Meseguer, José: A rewriting logic approach to operational semantics (2009)
  16. Balland, Emilie; Boichut, Yohan; Genet, Thomas; Moreau, Pierre-Etienne: Towards an efficient implementation of tree automata completion (2008)
  17. Boichut, Yohan; Genet, Thomas; Jensen, Thomas; Le Roux, Luka: Rewriting approximations for fast prototyping of static analyzers (2007)
  18. 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)
  19. Farzan, Azadeh; Meseguer, José: Partial order reduction for rewriting semantics of programming languages. (2007)
  20. Meseguer, José; Roşu, Grigore: The rewriting logic semantics project (2007)

1 2 next


Further publications can be found at: http://fsl.cs.illinois.edu/index.php/FSL_Publications