Paper Info
Title
Java memory model aware software validation
Abstract
The Java Memory Model (JMM) provides a semantics of Java multithreading for any implementation platform. The JMM is defined in a declarative fashion with an allowed program execution being defined in terms of existence of "commit sequences" (roughly, the order in which actions in the execution are committed). In this work, we develop OpMM, an operational under-approximation of the JMM. The immediate motivation of this work lies in integrating a formal specification of the JMM with software model checkers. We show how our operational memory model description can be integrated into a Java Path Finder (JPF) style model checker for Java programs.
Year
DOI
Venue
2008
10.1145/1512475.1512478
PASTE
Keywords
Field
DocType
aware software validation,declarative fashion,java path finder,java memory model,operational under-approximation,software model checker,java multithreading,program execution,java memory,style model checker,operational memory model description,java program,software validation,memory model,formal specification
Programming language,Computer science,Java annotation,Java concurrency,Real time Java,Real-time computing,Generics in Java,strictfp,Java Modeling Language,Java applet,Java
Conference
Citations 
PageRank 
References 
8
0.54
7
Authors
3
Name
Order
Citations
PageRank
Arnab De1271.93
Abhik Roychoudhury22449122.18
Deepak D'souza323917.90