Ideas, requests, problems regarding the Mobius site 
| Name | What? | Which repository? |
| Verification Condition Ast? | ||
| Bytecode Annotation Ast? | ||
| Bytecode Viewer? | ||
| Bytecode Editor? | ||
| Specification Ast? | ||
| Specification Editor? | ||
| Specification Refactorer? | ||
| Annotated Bytecode Compiler? | ||
| Verification Condition Generator? | ||
| Coq Backend? | Mobius VC AST -> Coq | sort.ucd.ie/cvsroot/escjava/MobiusDirectVCGen/ |
| Pvs Backend? | Mobius VC AST -> PVS | |
| Simplify Backend? | Mobius VC AST -> Simplify | |
| Yices Backend? | Mobius VC AST -> Yices | |
| Smt Lib Backend? | Mobius VC AST -> Smt Lib? | |
| Universes Typechecker? | ||
| Race Condition Checking Typechecker? | ||
| bico | BC -> Bicolano BC (Coq) | scm.gforge.inria.fr/svn/mobius/WP3/Task_3.6_Program_Verification_Environment/bico |
| FOL over source -> FOL over Bytecode | ||
| Direct VC Gen? (Source) | Source + FOL -> Mobius VC AST | sort.ucd.ie/cvsroot/escjava/MobiusDirectVCGen/ |
| Direct VC Gen? (Bytecode) | Bicolano BC + FOL(Coq) -> VC (Coq) | scm.gforge.inria.fr/svn/mobius/Formalisation/Logic |