Subsystems Under Development

• Bytecode Subsystem
• Sourcecode Subsystem^?
• Jml Subsystem^?
• Extended Static Checker Subsystem^?
• Automated Prover Subsystem^?
• Interactive Prover Subsystem^?
• Boogle Subsystem^?
• Race Condition Checker Subsystem^?
• Predicate Abstraction Subsystem^?
• Specification Generation Subsystem^?
• Proof Transforming Compiler Subsystem^?
• Compositional Typechecker Subsystem^?
• Certificate Subsystem^?

Components Under Development

Component Details

• Verification Condition Ast^?
• Bytecode Annotation Ast^?
• Bytecode Viewer^?
• Bytecode Editor^?
• Specification Ast^?
• Specification Editor^?
• Specification Refactorer^?
• Annotated Bytecode Compiler^?
• Verification Condition Generator^?
• Coq Backend^?
• Pvs Backend^?
• Simplify Backend^?
• Yices Backend^?
• Smt Lib Backend^?
• Universes Typechecker^?
• Race Condition Checking Typechecker^?

Semantics, Logics, and Typesystems Under Development

• Bicolano Semantics^?
• Mobius Base Logic^?
• Extended Static Checking Logics^?

General-purpose Eclipse Plugins

• Check Style Plugin
• Find Bugs Plugin
• Java NCSS Plugin
• Mylar Plugin
• Pmd Plugin
• Subclipse Plugin

Example Project Overviews

• Example Project Overview

Action Plans

WHAT	WHO	WHICH DIP?
which JML AST?	UCD + ETHZ	DIP2
Boogie PL? AST stuff	UCD \ Joe > ETHZ \ Peter	DIP2
Mobius VC AST	UCD > INRIA	DIP2
BC + BML -> Boogie PL?	ETHZ > UCD	DIP2
BC (+ BML) -> Mobius Bicolano [bico]	WU > INRIA \ David	DIP2
SC + JML (the JML tool suite AST ) -> Boogie PL? (AST)	WU > ETHZ	DIP2+
SC + JML -> BC + BML	UCD > INRIA esp Lilian	DIP2+
Boogie PL? -> Mobius VC AST	RUN > ETHZ + INRIA	DIP2+
Mobius VC AST -> Coq	INRIA > UCD	DIP2+
Mobius VC AST -> Simplify	UCD > INRIA	DIP2+
evaluate the Simplify -> Harvey translator	Joe@UCD	DIP2+
Mobius VC AST -> PVS	UCD > INRIA	DIP2+
Mobius VC AST -> Harvey	INRIA > UCD	DIP2+
Mobius VC AST -> SMT-LIB	UCD	DIP2+
later extension to multithreading	INRIA < UCD	DIP2+