Mobile Resource Guarantees

ได้เมลมาชวนไปสัมมนา (เค้าส่งหานศ.ทุกคนแหละ) เห็นว่าน่าสนใจดี เกี่ยวกับพวก mobile code เลยเอาลิงก์มาแปะ ตัวเองไปไม่ได้หรอก

Speakers: Alberto Momigliano and Lennart Beringer
Time: 4pm Friday 5th November 2004
Place: Room 4.03 Appleton Tower

Title: Automatic Certification of Resource Consumption

Abstract:

The Mobile Resource Guarantees (MRG) project is developing Proof-Carrying Code technology to endow mobile code with certificates of bounded resource consumption. These certificates should be generated by a compiler which, in addition to translating high-level programs into machine code, derives formal proofs based on programmer annotations and program analysis.

As the basis for reasoning and certificate generation, we employ a program logic for a subset of the JVM, implemented in Isabelle/HOL a' la Nipkow. Although, this has some niceties, such as the soundness and (relative) completeness, which we have formally verified, it proved less suited for concrete program verification, as it required a good deal of user interaction.

We here present a derived logic which is defined on top of the core logic and directly relates to our compile time analysis. It encodes at the JVM level the interpretation of the type system of Hofmann and Jost for heap space consumption. The complexity of the side conditions in the new logic is significantly lower than those in the base logic, making automatic verification feasible. In fact, a fairly naive tactic will solve all the examples we have considered so far.

If time permits, we will demo the whole MRG ``flow'', culminating in certificate generation.

หลังจากจดหมายข้างบน ก็มีส่งข้อความตามมาว่า:

Reminder. If there is sufficient interest, we could go to the pub afterwards.

Alan

คิดถึง T-T