Mikael Lagerkvists's
Master Thesis Homepage

Title	Machine Assisted Reasoning for Multi-Threaded Java Bytecode
Supervisor	Mads Dam
Abstract	In this thesis an operational semantics for a subset of the Java Virtual Machine (JVM) is developed and presented. The subset contains standard operations such as control flow, computation, and memory management. In addition, the subset contains a treatment of parallel threads of execution. The operational semantics are embedded into a $µ$-calculus based proof assistant, called the VeriCode Proof Tool (VCPT). VCPT has been developed at the Swedish Institute of Computer Science (SICS), and has powerful features for proving inductive assertions. Some examples of proving properties of programs using the embedding are presented.

Documents

• The slides for the presentation of my thesis are available.
• A draft of the thesis is also available. There are two variants, one with G5 as the page size (suitable for online viewing), and one with the same size of the type-block as the G5-sized, but with A4 as the page size (for easier printing).
  
  • thesis draft A4.
  • thesis draft G5.
• This zip-file contains my current array-theory and JVM-theory. To use these in a copy of VCPT unzip the file into the vcpt/lib/theories/ directory, creating two subdirectories Jvm and Array. To load the Jvm-theory into a running copy of VCPT, one executes

  - generate_accessors "Jvm";
  - load_theory "Jvm";
  - to_theory "Jvm";
  

  Note that the current version of VCPT available on the web is to old to handle the theory.

Finished parts

• A collection of predicates describing lists as arrays and the associated tactics with it. To get parametric behaviour simple macroexpansion is used once for each desired type.

Varsågod Gunnar: