IFIP Working Group 2.3
Programming Methodology

Home
News and Honors
Meetings
Members
Links

IFIP WG 2.3 meeting 47, Santa Fe

Logistics

Where:  Santa Fe Sage Inn, Santa Fe, New Mexico, USA.
When:  8-12 October 2007
Host:  Bob Baltzer

The pictures on this pages were taken by Carroll Morgan.  For more pictures from the meeting, Santa Fe, and the Albuquerque Balloon Fiesta, see the collections by Carroll Morgan and by Jim Horning et al.

Topics of discussion

• Daniel Jackson, Modelling with events
  
• Peter Müller, A Unified Framework for Verification Techniques for Object Invariants
  On joint work with Sophia Drossopoulou and Adrian Francalanza
  
  I will present a unified framework to describe verification techniques for object invariants. I will distil seven parameters, which characterize a verification technique, and identify sufficient conditions on these parameters under which a verification technique is sound. I will also define what it means for a technique to be modular. To illustrate the generality of our framework, I will instantiate it with verification techniques from the literature. The framework facilitates the assessment and comparison of the soundness, modularity, and expressiveness of these techniques.
  
  
• 
  Manfred Broy, Two Sides of Structuring Multi-Functional Software Systems:  Function Hierarchy and Component Architecture
  
  I would very much like to do a presentation about the material you have already seen which had made good progress in describing a structured view on the functionality of multi-functional systems.
   
• Jim Woodcock, Modelling Flash Memory
  
  Abstract: Flash memory is a kind of electrically erasable programmable read-only memory. Because it is non-volatile and relatively dense, it is often used as a substitute for magnetic disks, but it has two major limitations: the erasure block size is large and erasure causes memory cells to wear out. To overcome these limitations requires sophisticated algorithms and data structures, and I will give an overview of some of the problems involved. This work is part of the Verified Software Initiative pilot project to mechanically verify a POSIX-compliant file-store for critical applications. Insensitivity to shocks and changes in pressure and temperature and the lack of rotating parts make flash memory particularly attractive in space-slight missions.
  
  
• Shriram Krishnamurthi, Fun Implementing a SIGGRAPH paper:  Content-Aware Resizing of Images
  
  See http://www.seamcarving.com/.
  
• Eric C. R. Hehner, Incomputable Indeed
  
  I argued that there are no incomputable (or uncomputable) functions, see www.cs.utoronto.ca/~hehner/II.pdf.
  
• Annabelle McIver, What makes a good counterexample in (probabilistic) system verification?
  On joint work with Carroll Morgan and Carlos Gonzalia

  One of the successes of automated formal verification is in the generation of counterexamples which can lead to debugging specifications, or correcting faulty implementations. In probabilistic system design there is no tradition of using counterexamples in this way to aid system verification, and indeed there is not yet a standard notion of what a counterexample should be.

  In this talk I shall explore the question of what makes a "good" counterexample in system verification, using the context of probabilistic systems as a case study.

• Pamela Zave, Message Transmission, From the Top Down
  With thanks to Cliff Jones and Jim Woodcock
  
  
• 
  Peter Henderson, Located Functions
  
  
• Douglas R. Smith, Synthesis of Propositional Satisfiability Solvers
  
  
• Ernie Cohen, Short Problem:  Optimal Replay
  
  A solution written in BoogiePL (which verifies in 1.5 seconds with Boogie): ErniesBrkpts.bpl
   
  
• Rajeev Joshi, Formally Specifying Filesystems Robust to Hardware Failures
  Joint work with Gerard Holzmann and Alex Groce
  
  
• Rustan Leino, Designing a Type System for BoogiePL 2
  
  
• Michael Butler, Experience with Refining Event Atomicity
  
• William Cook, Models for Application Programming
  
  
• Clark Barrett, Satisfiability Modulo Theories
  
  
• Carroll Morgan, Horses for Courses:  Multi-paradigm Specification and Proof ...Eventually
  Reporting the work of Annabelle McIver and Ernie Cohen.
  
  Rabin's (distributed, probabilistic) mutual exclusion algorithm addresses the liveness of resource sharing by guaranteeing a probabilistic lower bound on the chance that a process competing for a shared resource will actually get it. At its core is a clever and unexpected mathematical "gem" around which the details of concurrency and overlapping executions are set: the gem is not obvious (to anyone but Rabin), but is nevertheless easily proved; the details of organising the concurrency, on the other hand, are obvious but not so easily proved. In fact there was an error in Rabin's original presentation.
  
  A rigorous proof/development of Rabin's algorithm seems very difficult; "Horses for Courses" means choosing the right tool for the job which, in this case, suggests a "multi-layered" technique with a different formalism for each layer. One layer uses probabilistic sequential techniques (pGCL, not much discussed in this talk); one -- the most intricate-- uses a probabilistic extension of Separation-and- Reduction technique (pKA, this talk); and one can be done in "ordinary maths" on a napkin.
  
  The talk summarises the history of the problem, and the proposed solution strategy (due to Annabelle and Ernie), and sketches what the progress so far has delivered. There turn out to be interesting links between pKA and other Kleene-style algebras invented for a wholly different purpose.
  
  
• Greg Nelson, P47: A Short Film
  
  I would like to lead a discussion on proof animation.  I will start the discussion off by showing an animated proof of approximately 5 minutes that I have produced over the last few months and ask for the reactions of the group.
   
  
• Ernie Cohen, Infinite Atomic Actions
  
  I will talk about how to extend sequential programming semantics to allow information to escape infinite loops. The interesting thing is that there turns out to be essentially no choice about the language used to specify state properties.
  
• Ian J. Hayes, Teleo-Reactive Systems and Timebands
  
  
• Greg Nelson, Choice of Choice Compositions in Guarded Commands
  
  
• Ernie Cohen, Pessimistic Testing
  
  Pessimistic testing is an approach to model-based testing of nondeterministic systems where you stop testing as soon as the system has a strategy to stop you from making progress.
  
  
• Ian Hayes, An Alternative Typing of Records:  moving typing information back from fields to records
  
  
• Ernie Cohen, The Hypervisor Verification Project
  
  I will talk about the Hypervisor Verification project, some of the tricks we're using, and some of the challenges we face. This would hopefully stir discussion.
   
  

Attendees

• Bob Balzer (host)
• Clark Barrett
• Manfred Broy
• Michael Butler
• Ernie Cohen
• William Cook
• Ian Hayes
• Eric Hehner
• Peter Henderson
• Jim Horning
• Daniel Jackson
• Rajeev Joshi
• Shriram Krishnamurthi
• Butler Lampson
• Rustan Leino
• Annabelle McIver
• Carroll Morgan
• Peter Müller
• Greg Nelson
• Michel Sintzoff
• Doug Smith
• Jim Woodcock
• Pamela Zave