ByteCodeSubsystem

These subsystems are responsible for reading and writing files in the BytecodeModelingLanguage (BML).

The mandatory requirements for the MOBIUS Bytecode Subsystems are:

BCEL with BML support (BMLLib)
pretty-print BML-annotated bytecode to screen and LaTeX/PDF (UCD)
BML-annotated bytecode compiler for JML level 0 and level C-annotated Java 1.4 source (JML2BML)
weakest-precondition calculus for sequential bytecode (INRIA)
weakest-precondition VC generator for sequential bytecode (INRIA)
Hoare logic for sequential bytecode (ETHZ)
Hoare logic VC generator for sequential bytecode (ETHZ?)
synchronization checker for arbitrary bytecode (UCD)
interaction with Coq instance for reasoning in MOBIUS logic(s)
- Bicolano formalization of VM (INRIA)
- MOBIUS base logic (Munich)
formalisation of sequential bytecode to guarded command language (ETHZ)
sequential bytecode to guarded command translator (ETHZ?)
Coq-specific PCC certificate generator

Secondary, desirable requirements for the MOBIUS Bytecode Subsystems include:

interactive bytecode editor with BML support (Umbra)
BML-annotated bytecode compiler for JML level 1 and level C-annotated Java 1.4 source (INRIA, UCD)
strongest-postcondition calculus for sequential bytecode (?)
strongest-postcondition generator for sequential bytecode (?)
general-purpose PCC certificate generator

BMLLib

Version: 9 Time: Tue Mar 17 16:48:41 2009 Author: alx (None) IP: 193.0.96.15