IFIP WG 2.3 meeting 48

Logistics

Where:  Cambridge, UK.
When:  21-25 July 2008
Host:  Tony Hoare

Topics of discussion

• Gary T. Leavens, Introduction to Aspect-Oriented Programming and its Reasoning Problems
  Based on joint work with Curtis C. Clifton, James Noble, Hridesh Rajan.  [slides]

  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 allowingadditions and changes to a program's execution. However, efficient reasoning about the functional behavior of AspectJ code 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. After describing these problems, I will give an overview of various techniques for solving them, including some of my own work.
  This talk in part describes joint work with Curtis Clifton, James Noble, and Hridesh Rajan and is based on work described in Clifton's Ph.D. dissertation. That work was supported in part by the US NSF under grants CCF-04-8078 and CNS 08-08913. For more details see http://www.eecs.ucf.edu/~leavens/modular-aop/

• Tony Hoare, Separation Logic and Trace Semantics
  Joint work with Peter O'Hearn.
• Tony Hoare and Ian Wehnman, Extending Trace Models [slides]
• 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 [try Orc]
• William R. Cook, Strategic Programming by Model Interpretation
• K. Rustan M. Leino and Peter Müller, Thread-local contributions [slides]
• 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
  Joint work with various people at U. Cambridge and INRIA
• 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 [pdf]
• 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
  Joint work with Radhia Cousot
• Pamela Zave and Eric Cheung, Compositional Control of IP Media
• Annabelle McIver, Carroll Morgan, and Carlos Gonzalia, Proofs and refutations for probabilistic systems [slides] [paper reference]

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)

IFIP WG 2.3 home page