Meeting 53
Host: Rustan Leino
Location: Kirkland, WA, USA
Dates: 16–20 July 2012
Talks
- Cliff Jones, Synergy between Separation Logic and Rely/Guarantee thinking
- Rustan Leino, Coinduction in a Language and Verifier
- Manfred Broy, A Logical Approach to Systems Engineering Artifacts and Traceability: From Requirements to Functional and Architectural Views
- Daniel Jackson, What’s Wrong with Git?
- Pete Manolios, Automated Synthesis of Software Architectures
- Wolfgang Paul, Theory for Multicore Hypervisor Verification
- Pamela Zave, A Practical Comparison of Alloy and Spin
- Jayadev Misra, Some Cute Programs
- Serdar Tasiran, Verifying Concurrent Programs with Relaxed Conflict Detection
Abstract
In a frequently-encountered pattern in concurrent programs, an operation first reads a large portion of shared data, then performs local computation, and finally writes to a small portion of shared data. This pattern leads to frequent conflicts between operations intended to appear atomic. To provide good performance alongside atomicity, implementations ranging from fine-grain locking to variations on transactional memory (TM) have been investigated. We present an approach for statically verifying TM-based solutions with programmer-directed conflict detection, including an abstraction recipe for sequential reasoning within transactions. - Peter Müller, Fractional Permissions without the Fractions
- Patrick Cousot, Proofs by Induction on Trace Covers
- Andreas Podelski, Inductive Data Flow Graphs
- Clark Barrett, Beyond DPLL(T): A New Boolean Search Framework for Model-Based Theory Reasoning
- Huibiao Zhu, Denotational Semantics for a Probability Timed Shared-Variable Language
- Michael Jackson, System Requirements: A Challenge? An Opportunity? Someone Else’s Problem?
- Bertrand Meyer, Concurrent Programming is Easy
- N. Shankar, Static Previrtualization
- N. Shankar, Proof of Jay Misra’s Tree-Reconstruction Program
- Ernie Cohen, Proof of Jay Misra’s Tree-Reconstruction Program
- Mark Utting, JStar: A New Parallel Programming Methodology
- Ethan Jackson, Formula: A Language for Abstractions; A Tool for Automated Analysis
- Ernie Cohen, A Separation Logic for Messages and Stuff in Orc
- Patrick Cousot, Hehner = (McIver+Morgan)^{-1}
Attendees
- Clark Barrett (acting secretary)
- Manfred Broy
- Ernie Cohen
- Patrick Cousot
- Jean-Christophe Filliâtre (WG 1.9)
- Daniel Jackson
- Michael Jackson
- Ethan Jackson (local observer)
- Cliff Jones
- Gary Leavens
- Rustan Leino (host)
- Pete Manolios (WG 1.9)
- Annabelle McIver
- Bertrand Meyer
- Jayadev Misra
- Michal Moskal (local observer)
- Peter Müller
- Wolfgang Paul (WG 1.9)
- Andreas Podelski (observer)
- Shaz Qadeer (local observer)
- Andrey Rybalchenko (WG 1.9)
- N. Shankar
- Serdar Tasiran (observer)
- Mark Utting
- Pamela Zave (chair)
- Huibiao Zhu (observer)