Bicolano and MOBIUS base logic

Bicolano

Bicolano (BYte COde LANguage in cOq) is concerned with the formalization of the Java Bytecode semantics with the Coq proof assistant.

This page gathers the main files of the formal development. The whole bundle of Coq files can be downloaded here and checked with Coq 8.0pl3.

Html files are listed here:

• Axiomatic definition of program syntax: Program.v
• Axiomatic definition of semantic domains: Domain.v
• Axiomatic definition of machine arithmetic: Numeric.v
• Small step semantics: SmallStep.v
• Global index.

MOBIUS base logic

MOBIUS base logic is the core program logic for bytecode and it relies on Bicolano JVM semantics. It is formalised with the Coq proof assistant. Its bundle with Coq files can be downloaded here and checked with Coq 8.0pl3.