Components

MOBIUS Components

WikiInclude(ComponentsExplanation)

Name	Languages Processed	Main Repository	Plugin Repository	Update Site
BML Library	BML	src/BmlLib/trunk	src/BmlLib_plugin
BONc	BON	src/bon
Coq Editor	Coq
Simplify	Mobius VC AST -> Simplify	src/simplify	src/simplify_plugin
Bico	BC -> Bicolano BC (Coq)	src/bico
DirectVCGen	Source + FOL -> Mobius VC AST	src/escjava/trunk/MobiusDirectVCGen
CCT		src/CCT/trunk
BML2BPL	BML -> BPL	src/BML_BPL_Translator
ETHZ JML2 Plugin	JML			ETHZ
Universe Type System	JML			ETHZ
ESC/Java2	Java + JML -> Mobius VC AST	src/escjava/trunk/ESCTools	src/escjava_plugin	UCD
Examples		src/examples
Freeboogie	BPL -> Mobius VC AST	src/freeboogie/trunk/FreeBoogie
Immutability Typechecker	JML
Javafe	Java + Bytecode -> Mobius VC AST	src/Javafe	src/Javafe_plugin
JML4	JML
JML2BML	JML -> BML	src/Jml2Bml/trunk
JML Class Library		src/Jmlclasslib
JML Folding	JML		src/JML_folding_plugin
Hawk	BON/JML/BML -> Hudson/Maven/JUnit test suites	src/Hawk src/test
Logging		src/logging
Plugin Library			libs/pluginlib
Prover Editor	Coq		src/provereditor_plugin	INRIA
Umbra	Java Bytecode	src/Umbra/trunk	src/Umbra_plugin	WU
Immutability Typechecker	Java + immutability annotations	src/Jimuva/trunk/Jimuva
RAJA	Resource Aware JAva (RAJA)			LMU
TLSAT	Trusted Labs Static analysis tool	Static analysis of Java bytecode against various security properties

For more information about non-MOBIUS components, see ExternalSubsystemsUpdateSites.

Templates for adding new typesystems and typecheckers are now available: TypecheckerTemplate, TypesystemTemplate.

Version: 43 Time: Wed Nov 12 09:09:12 2008 Author: mpavlova (None) IP: 213.30.180.226