Here are my detailed meeting notes:

** Madrid Meeting: Wed 21 June 2006

 - Randy: do we want full integration of the prover in the environment?

  Joe & Julien: for first deliverable, no.  later, a bit better, but
  not in the core mission of Mobius.

 - Mariela: because part of our mandate include a bytecode editor?

 - Marieke: nice but not mandatory for first deliverable

 - Jacek: it is really difficult to figure out what the users
   intentions are.

 - Joe: what about a GC/BoogiePL plugin?  we all agree that this is
   not necessary for now.

 - what is the intermediate format?  BoogiePL is the proposed
   intermediate representation.

 - Benjamin: thinks going from BoogiePL to Mobius base logic
   (MobiusBL) is really hard.  I want VCGens that go directly from
   source and/or bytecode to MobiusBL.

 - Peter: I don't understand why the VCGen at the bytecode level needs
   to be part of the TCB.

 - Benjamin: I wrote the VCGen from bytecode to MobiusBL in about a
   week in Coq so I don't think it is too hard.

 - Rustan: going through an encoding gives us more managable VCs

 - Julien: what about tracing the proof if we have one big VC?

 - Peter: why not just work on it on paper and do it when we are done
   with that?

 - balance between generating tons of VCs or one big one?

 - Marieke: if we go with IL...
   1. can we have tracability (yes)
   2. how is annotation generation impacted?
   3. when doing interactive proofs, do the proof obligations get
      really harder to understand?

 - Benjamin: some of the manipulations seen in existing BoogiePL
   generation seem to make things less clear to a prover.

 - Joe: just use good identifiers, labels, and comments.

 - Rustan showed some BoogiePL.

 - Joe: should we just use Benjamin's VCGen.

-- JosephKiniry - 27 Jun 2006