K-Java: A complete semantics of Java

Denis Bogdənaş, Grigore Rosu

Research output: Contribution to journalArticlepeer-review


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 multithreaded programs. Both the test suite and the static semantics are generic and ready to be used in other Java-related projects.

Original languageEnglish (US)
Pages (from-to)445-456
Number of pages12
JournalACM SIGPLAN Notices
Issue number1
StatePublished - Jan 2015


  • Java
  • K framework
  • Mechanized semantics

ASJC Scopus subject areas

  • Computer Science(all)

Cite this