Skip to topic
|
Skip to bottom
IST-15905
Tools Web
Mobius Public Home
Mobius Intranet
Tools Web Home
Overview
Tools Summary
Tools Contacts
Component Index
Related Tools
Download Tools
Scientific Issues
Tools Publications
Project Management
Development Schedule
Project Status
Documentation And Coding Standards
Latest News
Tools Meetings
Site Visits
GForge
Tools
Index
Search
Changes
RSS Feed
Statistics
Preferences
Edit Toolbar
Help
Start of topic |
Skip to actions
Here are my detailed meeting notes: <pre> ** 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. </pre> -- Main.JosephKiniry - 27 Jun 2006
End of topic
Skip to action links
|
Back to top
r1.1 :
Edit
|
Attach image or document
|
Printable version
|
Raw text
|
Page history
|
More actions
You are here:
Tools
>
ToolsMeeting21June2006
to top
Ideas, requests, problems regarding the Mobius site