Here are my detailed meeting notes:

** Thursday 22 June Meeting in Madrid

*** Agenda

**** VCGen (do we use Benjamin's VCGen for now?)

- Peter: Benjamin and I discussed the fact that we can just use the
  simple VCGen 

 1. do we just wrap Benjamin's VCGen as a IVE component?
  - takes bicolano spec to VC expressed in the Mobius base logic
  - right now it is all written in Coq
  - if we want to extract it, Coq removed everything in prop, so if we
    extract the current VCGen we get nothing.
  - if we just use bico then we don't need to extract.
 2. Benjamin does not mind trying to do the extract so
    some-mysterious-someone will do it.  Erik loves VCGen in Coq.

- Peter & Joe: start experimentation and development on VCGen to
  BoogiePL.  the core idea is to do both VCGens (from source code and
  bytecode) to the MobiusIR intermediate representation (e.g.,
  BoogiePL++?)

- Marieke: need experimental evidence about whether to generate one
  giant VC or many small VCs and which kind of generation is more
  appropriate for interactive vs. automatic verification.

- Joe: who is responsible for tactics (coqlets)?

  1. Benjamin & others at INRIA and UCD will work on this as part of
     3.6.  they managed to prove some goals automatically previous in
     the Jack work, so there is some expectation that they can get
     some automation.

- Joe: should we spend resources on generating VCs for automated
  provers?

  1. yes, we should do this levaging the experience and existing
     infrastructres in Jack and ESC/Java2.

- Erik: which of these translations do we need?

  1. VCGen at source and bytecode in Jack logic to the Jack proof
     obligation language (JPOL) intermediate representation, hence to
     B, Simplify, Harvey, PVS, and Coq
  2. VCGen from BML to JPOL
  3. generic VCGen at source in ESC logics to the ESC GC lang, hence
     to Simplify, Coq, PVS, SMT-LIB
  4. SC + JML to BC + BML (Mariela's thesis)
  5. on paper there is BC + BML to BoogiePL

  Mikolas: perhaps translate from existing IRs to BoogiePL?

  All: how do we get from SC to BoogiePL?

  Marike: do we go from SC to BoogiePL?

  Peter: we could go from GCs to BoogiePL?  we have quite a bit on
  paper and some partial implementation in the JML compiler for SC +
  JML (+ universes!) to BoogiePL.

  Peter: for BC + FOL etc to BoogiePL there is a lot on paper and a
  partial implementation in Coq.  we could finish this up (with lots
  of help from INRIA and UCD), adapting it to BML and then we just use
  it like Benjamin's VCGen (BenGen).

  Joe: who does BoogiePL to generic VC rep?  Benjamin: I could adapt
  my VCGen to BoogiePL!  Joe: we could implement this in Java also,
  taking BoogiePL specs to the generic VC rep.

  Mikolas: does the bytecode need to have a reducable control flow
  graph?  what other assumptions are there about the bytecode.
  Mariela and Peter: yes, we need it.  Joe: also the bytecode cannot
  mention any Java constructs that are not covered in the semantics.

  Marieke: what about the SC+JML to BML compiler?  Robin is going to
  do a code review of the BML implementation.  currently we only
  translate desugared specs, but maybe we need to make the mapping
  from JML_0 to BML to be 1:1.  Joe: keeping more structure at the BML
  level will make for much easier interactive program verification in
  the long run and doing so does not hurt the ETH folks because they
  have made no assumptions about the source of their BoogiePL target
  translation.

  - Summary of responsibilities, i.e., who does what

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

**** what about the tools that Peter keeps mentioning?

 - Peter: I was talkinga about three inference tools for the Universe
   type system (relates to 2.5 and 3.7).  they are good for different
   situations (to answer Marieke).  one looks at heap dumps, thus does
   not depend upon annotations at all.  the other two do source code
   analysis but really like having some annotations.  Joe: which AST
   do the latter two work on?  Peter: on the JML AST! Wheee!

 - Peter: Sorry.  The Jive tool also exists but is not interesting for
   Mobius; but we have a lot of experience translating Java to a
   program logic so we are smart.  Joe: Right?  Peter: Ha!

**** bico

 - update from WU guys: translator that takes a bytecode classfile and
   spits out Bicolano.  it will be ready in about a week or ten.
   there are no docs unfortunately, and few test cases....  Radu: Is
   that right?  Jacek: Yes. Ha!

**** umbra

 - update from WU guys: Eclipse plugin to print and modify bytecode,
   including comments in BC, which may one day be BML specs.  we'll
   stick with using BCEL for the moment.  we need assistance from
   INRIA to implement support for BML (email support from Lilian,
   Mariela, and maybe Julien).  Marieke: there is work in 3.1 and
   Mariela has lots and lots of stuff to show you.

**** runtime exceptions

 - Peter: summarizes the two different ways we can deal with the
   program logic: either deal with runtime exceptions just like Java
   does; or we disallow runtime expections explicitly (as an
   assumption) then we have simpler VCs.

 - Lots of discussions followed by an action item for Peter to send a
   updated version of his initial email with a concrete revised spec
   example, e.g., java.lang.System.arraycopy() since not everyone is
   convinced.

 - Peter promised to add the slides to the wiki.

 - Lots of discussion took place at coffee about this point and we are
   still not at all convinced.  Poor Peter.  Radu thinks he is
   convinced with Erik's help, so Radu is Peter's Proxy.  Erik: Does
   the Peter-Principle apply here?...

*** BML

 - Marieke: At some point Gilles came into my office and said, "Once
   upon a time..."  Gilles does not tell stories, he just has good
   ideas.  There should be a BML strike force to define BML precisely,
   ensure that the BML library is perfect and shiney, it can include
   people not in Mobius, etc.

 - Mikolas: Because I am interested in assertion generation, which
   gets done at the IR, where there are things like a heap, which
   cannot be expressed in JML today.  Should this be part of BML?

 - Mariela: There are some ways to talk about the stack, but they do
   not normally used in a contract, but might be used in an
   assertion.

 - Erik: there is a \reach expression for which you can define a
   semantics.

 - Joe: there is an explicit heap model in some of the ESC and Mobius
   logics too.

 - Marieke: in the deliverable for 3.1 I talk about BML which is JML_0
   + a bit of JML_1.  We need to think a bit more about this, what do
   we want, etc.  We need an expression grammar in the appendix of the
   deliverable.  Robin told me he'd be happy to look at that with me.

 - BML Strike Force Members:
   1. Marieke (QUEEN) [HARDCORE]
   2. Mariela (DUTCHESS) [HARDCORE]
   3. Robin (ROGUE) [HARDCORE]
   4. Erik (PRINCESS) [HARDCORE]
   5. Jacek (JACK) 
   6. Aleksy (EX-POPE) 
   9. Julien (NINJA)
   10. Peter (POPE)
   11. Joe only CCed
   12. Gilles only CCed
   13. Benji CCed
   14. Mobius-external people?  David Cok?  Patrice Chalin?  

 - Erik: only get someone external that is interested in
   bytecode-level stuff.

 - Radu: what is the output of HARDCORE?  Marieke: just a
   well-specified document describing BML in gory detail.

 - To do items:
   1. Marieke: create a mobius-bml mailing list
   2. Marieke: subscribe HARDCORE members to get them started
   3. HARDCORE: members come up with initial proposal/spec (no impl)
   4. Marieke: email JML users/developers to find someone who might be
      interested in this topic.

 - Mariela then gave a demonstration of the current BML library's
   capabilities in Jack.

-- JosephKiniry - 27 Jun 2006