Home » #53 Kirkland, WA, USA

#53 Kirkland, WA, USA

Where:  Woodmark Hotel, Kirkland, WA, USA
When:  16-20 July 2012
Host:  Rustan Leino

Topics of discussion

  • Cliff Jones, Synergy between Separation Logic and Rely/Guarantee thinking [slides]
  • Rustan Leino, Coinduction in a Language and Verifier [slides]
  • Manfred Broy, A Logical Approach to Systems Engineering Artifacts and Traceability: From Requirements to Functional and Architectural Views [slides]
  • Daniel Jackson, What’s Wrong with Git?, with Alcino Cunha, Jonathan Edwards, Eunsuk Kang, and Andrea Mocci [slides]
  • Pete Manolios, Automated Synthesis of Software Architectures
  • Wolfgang Paul, Theory for Multicore Hypervisor Verification, joint work with E. Cohen, S. Schmaltz, … [slides]
  • Pamela Zave, A Practical Comparison of Alloy and Spin [paper]
  • Jayadev Misra, Some Cute Programs [slides]
  • Serdar Tasiran, Verifying Concurrent Programs with Relaxed Conflict Detection, joint work with Tayfun Elmas, Ismail Kuru, Omer Subasi [slides]
    • 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. We show how static correctness proofs of such programs can be streamlined. The key challenge is that one can no longer reason sequentially within transactions. To address this challenge, we provide an abstraction recipe that restores the ability to reason sequentially. We demonstrate our approach by mechanically verifying examples from the STAMP benchmark suite.
  • Peter Müller, Fractional Permissions without the Fractions, joint work with Stefan Heule, Rustan Leino, Malte Schwerhoff, Alex Summers
  • Patrick Cousot, Proofs by Induction on Trace Covers, joint work with Radhia Cousot [slides4up, Papers: POPLOOPSLA]
  • Andreas Podelski, Inductive Data Flow Graphs, joint work with Azadeh Farzan, Zachary Kincaid [slides]
  • Clark Barrett, Beyond DPLL(T): A New Boolean Search Framework for Model-Based Theory Reasoning, joint work with Dejan Jovanović, Leonardo de Moura [slides]
  • Huibiao Zhu, Denotational Semantics for a Probability Timed Shared-Variable Language, joint work with Jeff Sanders, Jifeng He, Shengchao Qin [slides]
  • Michael Jackson, System Requirements: A Challenge? An Opportunity? Someone Else’s Problem? [slides]
  • Bertrand Meyer, Concurrent Programming is Easy [Slides: pdfpptx]
  • N. Shankar, Static Previrtualization, joint work with Drew Dean, Bruno Dutertre, Ashish Gehani, Gregory Malecha, Ian Mason, Sam Owre, Hassen Saïdi [slides]
  • N. Shankar, Proof of Jay Misra’s Tree-Reconstruction Program [included in slides link above]
  • Ernie Cohen, Proof of Jay Misra’s Tree-Reconstruction Program [slides]
  • Mark Utting, JStar: A New Parallel Programming Methodology [slides]
  • Ethan Jackson, Formula: A Language for Abstractions; A Tool for Automated Analysis
  • Ernie Cohen, A Separation Logic for Messages & Stuff in Orc [slides]
  • Patrick Cousot, Hehner = (McIver+Morgan)-1 | McIver+Morgan = (Hehner)-1, joint work with Michael Monerau [slides4upPaper]

Congratulations to Shriram Krishnamurthi, winner of the SIGPLAN 2012 Robin Milner Young Researcher Award.

Congratulations to Rustan Leino and Greg Nelson, two of the authors of a paper that won the SIGPLAN most influential PLDI paper award.


From Monday, July 16, to Wednesday, July 18, the meeting was held jointly with working group 1.9 (WG 1.9).

  • Clark Barrett (acting secretary)
  • Manfred Broy
  • Ernie Cohen
  • Patrick Cousot
  • Jean-Christophe Filliatre (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)