Meeting 52

Host: Michael Butler
Location: Winchester, UK
Dates: 19–23 September 2011

Talks

• Pamela Zave, Compositional network mobility
• Michael Butler, Relating problem structure and solution structure in Event-B refinement
• Cliff Jones, Inferring intent from proof attempts: AI4FM project
• Jim Woodcock, The Safety-Critical Java Memory Model: A Formal Account
• Annabelle McIver, Ad hoc routing in wireless networks using algebra
• Serdar Tasiran, Simplifying linearizability proofs using reduction and abstraction
• Tony Hoare, Algebra of concurrent programming
• Peter Henderson, Geometry and abstraction
• Perdita Stevens, Towards modularity and compositionality in the engieneering of model translations
• Willem Visser, Symbolic execution: A quest for nails
• Andreas Podelski, Correctness requirements for correctness requirements
• Huibiao Zhu, Denotational semantics and its algebraic generation for an event-driven system-level language
• John Colley, Feedback loop verification in low-power microprocessor pipelines
• Michael Jackson, Some ideas about developing and comprehending requirements for computer-based systems
• Sophia Drossopoulou, Zeno: An automated theorem prover for functional programs
• Gennaro Parlato, The tree-width of auxiliary storage
  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
• Ian J. Hayes, Requirements modelling and integration
• Carroll Morgan, A notation for probability distributions
• Cliff Jones, Possible values: an additional notation for assertions

Attendees

• 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)