IFIP WG 2.3 meeting 47, Santa Fe
Logistics
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 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 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, 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 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