Where: Santa Fe Sage Inn, Santa Fe, New Mexico, USA.
When: 812 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 FrancalanzaI 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 MultiFunctional 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 multifunctional systems.
 Jim Woodcock, Modelling Flash Memory
Abstract: Flash memory is a kind of electrically erasable programmable readonly memory. Because it is nonvolatile 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 POSIXcompliant filestore for critical applications. Insensitivity to shocks and changes in pressure and temperature and the lack of rotating parts make flash memory particularly attractive in spaceslight missions.
 Shriram Krishnamurthi, Fun Implementing a SIGGRAPH paper: ContentAware Resizing of Images
See http://www.seamcarving.com/.  Eric C. R. Hehner, Incomputable Indeed
I argued that there are no incomputable (or uncomputable) functions, seewww.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 GonzaliaOne 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: Multiparadigm 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 “multilayered” 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 Separationand 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 Kleenestyle 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, TeleoReactive Systems and Timebands
 Greg Nelson, Choice of Choice Compositions in Guarded Commands
 Ernie Cohen, Pessimistic Testing
Pessimistic testing is an approach to modelbased 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