Meeting 48

Host: Tony Hoare
Location: Cambridge, UK
Dates: 21–25 July 2008

Talks

• Gary T. Leavens, Introduction to Aspect-Oriented Programming and its Reasoning Problems
  Abstract

  How to modularize code in the face of cross-cutting concerns is a pressing problem for large software systems. Aspect-oriented languages, such as AspectJ, help solve this problem by allowing additions and changes to a program's execution. However, efficient reasoning about the functional behavior of AspectJ code is difficult. In this talk I will introduce: the design and programming problems addressed by aspect-oriented techniques, the solutions adopted by aspect-oriented languages (in particular by AspectJ), and some of the problems that such solutions cause for efficient reasoning. Based on joint work with Curtis Clifton, James Noble, and Hridesh Rajan.
• Tony Hoare, Separation Logic and Trace Semantics
• Tony Hoare and Ian Wehnman, Extending Trace Models
• Michael Butler, Structuring Event-B refinements with Jackson Structure Diagrams (JSD)
• Rajeev Joshi, “Non Local” Commutativity
• David Kitchin, Evan Powell, Jayadev Misra, Simulation, Orchestration and Logical Clocks
• William R. Cook, Strategic Programming by Model Interpretation
• K. Rustan M. Leino and Peter Müller, Thread-local contributions
• Douglas R. Smith, Calculating Refinements for System Design
• Michel Sintzoff, Generic synthesis of control policies for various objectives in infinite transition systems
• Peter Henderson, Abstraction - the tool that makes big things small
• Peter Sewell, The semantics of x86 multiprocessor machine code
• Philippa Gardner, Gareth Smith, Mark Wheelhouse, and Uri Zafaty, Local Hoare Reasoning about Data Update
• Clark Barrett, Bit-Precise Reasoning Using Satisfiability Modulo Theories
• Jean-Raymond Abrial, Pedagogical Research in Formal Methods
• Ian J. Hayes, Towards Reasoning About Teleo-Reactive Systems
• Byron Cook and Andreas Podelski, Proving termination of recursive programs, without the recursion
• Eric C. R. Hehner, a Probability Perspective
• Ron van der Meyden, Architectural Refinement
• Ralph-Johan Back, Teaching formal methods in High School
• Patrick Cousot, Calculational Design of Semantics of the Eager Lambda-Calculus by Abstract Interpretation
• Pamela Zave and Eric Cheung, Compositional Control of IP Media
• Annabelle McIver, Carroll Morgan, and Carlos Gonzalia, Proofs and refutations for probabilistic systems

Attendees

• Jean-Raymond Abrial
• Ralph Back
• Clark Barrett (observer)
• Michael Butler
• Byron Cook (local observer)
• William Cook (observer)
• Patrick Cousot
• Phillipa Gardner (observer)
• John Harrison
• Ian Hayes
• Eric Hehner
• Peter Henderson
• Tony Hoare (host)
• Michael Jackson
• Cliff Jones
• Rajeev Joshi (observer)
• Gary Leavens
• Rustan Leino (secretary)
• Jayadev Misra
• Caroll Morgan
• John Reynolds
• Peter Sewell (local observer)
• Michel Sintzoff
• Douglas Smith (observer)
• Ron van der Meyden (observer)
• Ian Wehrman (local observer)
• Pamela Zave (chair)