IFIP WG 2.3 meeting 52

Logistics

Where:  Winchester Guildhall (and Winchester Royal Hotel), Winchester, UK
When:  19-23 September 2011
Host:  Michael Butler

Here are some photos of the excursion, courtesy Michael Butler.

Topics of discussion

• Pamela Zave, Compositional network mobility, joint work with Jennifer Rexford [slides]
• Michael Butler, Relating problem structure and solution structure in Event-B refinement [slides]
• Cliff Jones, Inferring intent from proof attempts: AI4FM project [slides]
• Jim Woodcock, The Safety-Critical Java Memory Model: A Formal Account, with Ana Cavalcanti and Andy Wellings [slides]
• Annabelle McIver, Ad hoc routing in wireless networks using algebra, with Peter Hoefner [slides]
• Serdar Tasiran, Simplifying linearizability proofs using reduction and abstraction, with Tayfun Elmas, Ali Sezgin, Omer Subasi, and Shaz Qadeer [slides]
• Tony Hoare, Algebra of concurrent programming [slides]
• Peter Henderson, Geometry and abstraction [slides]
• Perdita Stevens, Towards modularity and compositionality in the engieneering of model translations [slides]
• Willem Visser, Symbolic execution: A quest for nails [slides]
• Andreas Podelski, Correctness requirements for correctness requirements, joint work with Amalinda Post, Jochen Hoenicke, and Sergiy Bogomolov [slides]
• Huibiao Zhu, Denotational semantics and its algebraic generation for an event-driven system-level language [slides]
• John Colley, Feedback loop verification in low-power microprocessor pipelines [slides]
• Michael Jackson, Some ideas about developing and comprehending requirements for computer-based systems [slides]
• Sophia Drossopoulou, Zeno: An automated theorem prover for functional programs [slides]
• Gennaro Parlato, The tree-width of auxiliary storage [slides]
  • Abstract: The talk is about a generalization of various results on the decidability of emptiness for several restricted classes of sequential and distributed automata with auxiliary storage (stacks, queues) that have recently been proved. Our generalization relies on reducing emptiness of these automata to finite-state graph automata (without storage) defined on monadic second-order (MSO) definable graphs of bounded tree-width, where the graph structure encodes the mechanism provided by the auxiliary storage. Our results outline a uniform mechanism to derive emptiness algorithms for automata, explaining and simplifying several existing results, as well as proving new decidability theorems.
• K. Rustan M. Leino, Program synthesis with Jennisys, joint work with Aleksandar Milicevic [slides]
• Ian J. Hayes, Requirements modelling and integration [slides]
• Carroll Morgan, A notation for probability distributions [summary in PDF]
• Cliff Jones, Possible values: an additional notation for assertions [slides]

Participants

• Ralph Back
• Michael Butler (host and vice chair)
• John Colley (local observer)
• Sophia Drossopoulou (observer)
• Ian Hayes
• Peter Henderson
• Tony Hoare
• Michael Jackson
• Cliff Jones
• Rustan Leino (secretary)
• Annabelle McIver
• Carroll Morgan
• Gennaro Parlato (local observer)
• Andreas Podelski (observer)
• Reza Sarshogh (local observer)
• Perdita Stevens (observer)
• Serdar Tasiran (observer)
• Willem Visser (observer)
• Jim Woodcock (observer)
• Pamela Zave (chair)
• Huibian Zhu (observer)

IFIP WG 2.3 home page