• Title of article

    Executable JVM model for analytical reasoning: A study

  • Author/Authors

    Hanbing Liu، نويسنده , , J. Strother Moore، نويسنده ,

  • Issue Information
    دوهفته نامه با شماره پیاپی سال 2005
  • Pages
    22
  • From page
    253
  • To page
    274
  • Abstract
    To study the properties of the Java Virtual Machine (JVM) and Java programs, our research group has produced a series of JVM models written in a functional subset of Common Lisp. In this paper, we present our most complete JVM model from this series, namely, M6, which is derived from a careful study of the J2ME KVM [Connected Limited Device Configuration (CLDC) and the K Virtual Machine, ] implementation.
  • Keywords
    Simulator , Program verification , Software specification , Bytecode verification , JVM model , Formal Methods , Virtual machine
  • Journal title
    Science of Computer Programming
  • Serial Year
    2005
  • Journal title
    Science of Computer Programming
  • Record number

    1079807