Meeting 47

Host: Bob Baltzer
Location: Santa Fe, NM, USA
Dates: 8–12 October 2007

Talks

  • Daniel Jackson, Modelling with events
  • Peter Müller, A Unified Framework for Verification Techniques for Object Invariants
    Abstract 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
  • 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.
  • Shriram Krishnamurthi, Fun Implementing a SIGGRAPH paper: Content-Aware Resizing of Images
  • Eric C. R. Hehner, Incomputable Indeed
    Abstract I argued that there are no incomputable (or uncomputable) functions.
  • Annabelle McIver, What makes a good counterexample in (probabilistic) system verification?
    Abstract 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
  • Peter Henderson, Located Functions
  • Douglas R. Smith, Synthesis of Propositional Satisfiability Solvers
  • Ernie Cohen, Short Problem: Optimal Replay
  • Rajeev Joshi, Formally Specifying Filesystems Robust to Hardware Failures
  • 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
    Abstract 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" which 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. A rigorous proof/development 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.
  • Greg Nelson, P47: A Short Film
    Abstract 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
    Abstract 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
    Abstract 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
    Abstract I will talk about the Hypervisor Verification project, some of the tricks we're using, and some of the challenges we face.

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
This site uses Just the Docs, a documentation theme for Jekyll.