K-Java: A Complete Semantics of Java. This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology. In order to maintain clarity while handling the great size of Java, the semantics was split into two separate definitions -- a static semantics and a dynamic semantics. The output of the static semantics is a preprocessed Java program, which is passed as input to the dynamic semantics for execution. The preprocessed program is a valid Java program, which uses a subset of the features of Java. The semantics is applied to model-check multi-threaded programs. Both the test suite and the static semantics are generic and ready to be used in other Java-related projects.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
- Moore, Brandon; Peña, Lucas; Rosu, Grigore: Program verification by coinduction (2018)
- Arusoaie, Andrei; Ciobâcă, Ştefan; Lucanu, Dorel; Rosu, Grigore; Rusu, Vlad; Şerbănuţă, Traian-Florin: Program logics and their applications (2017)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Ciobâcă, Ştefan; Lucanu, Dorel; Rusu, Vlad; Roşu, Grigore: A language-independent proof system for full program equivalence (2016)
- Arusoaie, Andrei; Lucanu, Dorel; Rusu, Vlad: Symbolic execution based on language transformation (2015)
- Bogdanas, Denis; Roşu, Grigore: K-Java: a complete semantics of Java (2015)
- Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei; Nowak, David: Verifying reachability-logic properties on rewriting-logic specifications (2015)
- Roşu, Grigore: From rewriting logic, to programming language semantics, to program verification (2015)