K-Java: A complete semantics of Java

Denis Bogdənaş, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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)
Title of host publicationPOPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages445-456
Number of pages12
ISBN (Electronic)9781450333009
DOIs
StatePublished - Jan 14 2015
Event42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 - Mumbai, India
Duration: Jan 12 2015Jan 18 2015

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume2015-January
ISSN (Print)0730-8566

Other

Other42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
Country/TerritoryIndia
CityMumbai
Period1/12/151/18/15

Keywords

  • Java
  • K framework
  • Mechanized semantics

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'K-Java: A complete semantics of Java'. Together they form a unique fingerprint.

Cite this