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