|
|
|---|
|
|
|
|---|
J S. Moore, “Proving
Theorems about Java and the JVM with ACL2”, in M. Broy and
M. Pizka, editors, Models, Algebras and Logic of Engineering Software,
IOS Press, Amsterdam, pp. 227-290, 2003.
Relevance: M5: a JVM model with method invocation,
classes, and threads, with some example proofs including about
mutual-exclusion
This paper was the basis for a series of talks at the 2002 Marktoberdorf
Summer School, Germany. Among other topics, it describes the M5 JVM
model (ACL2 script