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:

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.

Revision: r1.9 - 24 Feb 2009 - 16:22 - GustavoPetri
Bicolano > WebHome
Ideas, requests, problems regarding the Mobius site QUESTION?