Here is a recapitulation of where are the components and what they do.

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