Skip to topic | Skip to bottom
... Mobius IST-15905


Start of topic | Skip to actions

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

Example Project Overviews

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+



You are here: Tools > ComponentIndex

to top

Ideas, requests, problems regarding the Mobius site QUESTION?