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