-
Notifications
You must be signed in to change notification settings - Fork 8
ToolsMeeting21June2006
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...
- can we have tracability (yes)
- how is annotation generation impacted?
- 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.
-- JoeKiniry - 27 Jun 2006
Version: 2 Time: Sun Sep 16 21:22:15 2007 Author: dcochran (dcochran) IP: 193.120.116.177