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+ |