Executable JVM model for analytical reasoning: A study

DOI10.1016/j.scico.2004.07.004zbMath1077.68560OpenAlexW3032775210MaRDI QIDQ2566223

Han-Bing Liu, J. Strother Moore

Publication date: 22 September 2005

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.scico.2004.07.004

zbMATH Keywords

Java programsJava virtual machine

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items

CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, A mechanical analysis of program verification strategies, The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4

Uses Software

• CLDC