Meeting 49
Host: Daniel Jackson
Location: Boston, MA, USA
Dates: 8–12 June 2009
Talks
- 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
- 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?
- Peter Müller (with Rustan Leino), A Chalice example
- Rustan Leino (with Peter Müller), Locks, channels, deadlock freedom, progress
- Peter Henderson, Modular reasoning about open architectures
- 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
Attendees
- 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)