IFIP WG 2.3 meeting 49

Logistics

Where:  MIT
When:  8-12 June 2009
Host:  Daniel Jackson

Venue:  Kendall Hotel

Daniel Jackson took some pictures from the meeting, and Rajeev Joshi took these pictures.

Topics of discussion

• Peter Müller (with Rustan Leino)
  A basis for verifying multi-threaded programs
• William Cook (et al.)
  Slice, Partition and Reforestation for Data Access and Distribution
• Pamela Zave
  Two great products of MIT:  Reasoning about Chord with Alloy
• Michael Butler
  Structured Event Refinement [slides]
• Ioannis T. Kassios
  Theories as Specifications
• Daniel Jackson and Eunsuk Kang
  Dependence and dependability
• Bertrand Meyer (with Emmanuel Stapf and Alexander Kogtenkov)
  Avoid a void
• Bill McKeeman
  Can a tiny compiler-compiler grow into something useful? [slides]
• Peter Müller (with Rustan Leino)
  A Chalice example
• Rustan Leino (with Peter Müller)
  Locks, channels, deadlock freedom, progress [slides]
• Peter Henderson
  Modular reasoning about open architectures [slides]
• Annabelle McIver
  Program development with Secure Refinement
• Rajeev Joshi
  Analyzing telemetry logs
• Armando Solar-Lezama
  A Quick Introduction to Sketching
• Ernie Cohen
  Verifying Concurrency in C
• Mark Utting (with John Cleary)
  JStar: A Declarative Language for a Parallel World
• Gary T. Leavens
  Preventing Cross-Type Aliasing to Promote Weak Behavioral Subtyping
• Shriram Krishnamurthi (et al.)
  Alchemy

Participants

• Michael Butler (vice chair)
• Ernie Cohen
• William Cook (observer)
• Peter Henderson
• Daniel Jackson (host)
• Michael Jackson
• Rajeev Joshi (observer)
• Yannis Kassios (observer)
• Shriram Krishnamurthi
• Butler Lampson
• Gary Leavens
• Rustan Leino (secretary)
• Doug McIlroy
• Annabelle McIver
• Bill McKeeman
• Bertrand Meyer
• Peter Müller
• Joe Near (local observer)
• Derek Rayside (local observer)
• Michel Sintzoff
• Armando Solar-Lezama (local observer)
• Mark Utting
• Pamela Zave (chair)

IFIP WG 2.3 home page