TY - GEN
T1 - K-Java
T2 - 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
AU - Bogdənaş, Denis
AU - Roşu, Grigore
N1 - Publisher Copyright:
Copyright © 2015 by the Association for Computing Machinery, Inc. (ACM).
Copyright:
Copyright 2015 Elsevier B.V., All rights reserved.
PY - 2015/1/14
Y1 - 2015/1/14
N2 - 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.
AB - 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.
KW - Java
KW - K framework
KW - Mechanized semantics
UR - http://www.scopus.com/inward/record.url?scp=84939539939&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84939539939&partnerID=8YFLogxK
U2 - 10.1145/2676726.2676982
DO - 10.1145/2676726.2676982
M3 - Conference contribution
AN - SCOPUS:84939539939
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 445
EP - 456
BT - POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PB - Association for Computing Machinery
Y2 - 12 January 2015 through 18 January 2015
ER -