Where: Prato, Italy
When: 6-10 September 2004
Host: Bertrand Meyer
Here is an overview of Prato and the
Monash center. Here are many more
pictures, courtesy of Carroll Morgan and Gary Leavens.
Topics of discussion
Cliff Jones, Beyond "Verifying Compiler".
Discussion of the Grand Challenge of a Verifying Compiler (or, a Verifying
One conclusion: The "Verifying Compiler" should not be concerned with
verifying the absence of bugs, but help with the design of software.
- Donald MacKenzie's 1995 work that analyzes the failures that led to some
- Jones, Hoare, and Randell: "Extending the horizons of DSE [Grand Challenge GC-6 on "Dependable Systems Evolution", accepted by UKCRC]"
- Gary Leavens, Alias-Free Formal Parameters
Aliasing among formal parameters, and among formals and globals,
causes problems for both optimization and reasoning; such aliases are
a source of subtle errors in programs. Whole-program static analysis
could provide knowledge about such aliasing, but it is non-modular,
expensive, and conservative. All of these characteristics are
undesirable for reasoning.
I will describe a small extension to Java and JML that leads to
significantly better optimization opportunities for a compiler and
allows modular reasoning. The extension allows aliasing among
arguments and globals at the call site, but guarantees there will be
no overlap among arguments and globals inside method bodies, and also
allows methods to have specifications that "work" for overlapping
arguments. This is done by having multiple bodies for each procedure,
up to one for each aliasing pattern. Procedure calls are
automatically dispatched to the body that matches the run-time
aliasing pattern among the actual parameters and the globals.
This talk is based on joint work with Medhat Assaad and Olga
Antropova. Thanks to Jim Horning, Murali Sitaraman, Greg Kulczycki,
William Ogden, and Bruce Weide for discussions of related topics.
This work is supported in part by the US National Science Foundation
under grants CCR-9803843, CCR-0097907, CCR-0113181, CCF-0428078, and
- Peter Müller, Modular verification of object and module invariants
(joint work with Rustan Leino)
The talk describes a methodology for specifying and verifying
object-oriented programs, using object invariants to specify the consistency
of data and using ownership to organize objects into dynamic contexts.
Object invariants can describe a large variety of properties, including
properties of cyclic data structures. The methodology is designed to
allow modular reasoning, even in the presence of subclasses and callbacks.
Module invariants describe properties of variables that are shared by
several objects. I would like to discuss how the presented methodology for
object invariants can be adapted to cover module invariants.
- Bertrand Meyer, The Dependent Delegate Dilemma
- Pamela Zave, A formal model of addressing for interoperating networks.
- Annabelle McIver, Optimal strategies for two-player parity games
In this talk I will discuss the problem of finding optimal strategies
for two-player games.
Game models of programs can be useful in the specification and analysis of
temporal-style properties. In such models players compete to optimise
some specified reward function. Of particular interest are the
strategies they employ for winning the game and, amongst those, "memoriless"
strategies --- those which only depend on the current game configuration ---
are arguably the most useful of all.
It has recently been proved that in the stochastic parity-game setting
optimal memoriless strategies exist for each player --- and in fact they can
be assumed to be "pure", ie. they do not need to be randomised.
Unfortunately determining those optimal memoriless strategies can be
I will show how optimal memoriless strategies can be computed reasonably
simply, provided that non-pure strategies are an acceptable solution.
- Michael Jackson, The problem of the banker with 52 cards.
A “banker” has an ordinary 52-card deck of cards. You have some
positive amount of money. The banker decides on the order of the
cards. Before the banker turns each card over, you place a bet.
You put some proportion of you money on “red” and the rest on “black”.
After the banker turns over the card, you lose the money you bet on the
losing color, and double the money you put on the winning color.
Design a strategy that maximizes your guaranteed gain, and prove this
- Ian Hayes, Finding Faults
Examining systematic methods for detecting faults in components, including
- Michael Butler, Semantics and atomicity for long-running transactions
Long-running transactions lack the atomicity of ACID transactions.
Instead of rollbacks and checkpoints, compensation is used to recover from
error. The development of a trace semantics has lead to a structured
design for a language of long-running transactions and also to a rational
basis for the use of compensation in which a degree of atomicty can be
Cliff Jones, Towards a development method, "Splitting atoms safely".
Wanted: a method that provides the fiction of atomicity. Can
atomicity be used in program design? Wants atomicity refinement,
especially in combination with data refinement.
- New (and clear!) database book by Gerhard Weikum
- "Atomicity in system design and execution", Dagstuhl seminar, April 2004
- Mark Utting, Model-Based Testing
In this talk, I will describe the problems of generating good test suites
from formal specifications (pre/post style). The goal is to build a
practical tool (the LTG -- Leirios Test Generator) that engineers can use to
semi-automatically generate tests from B, Z, JML, UML or Statechart
- Bertrand Meyer, The mathematics of object computation.
- Jean-Raymond Abrial, Developing discrete transition systems.
(1) Refinement of Stuttering steps: skip or keep (or both).
Stuttering steps are usually considered to be refinement of skip. In
certain cases, it is interesting however to think of them as being a
refinement of (a sort of) keep (the action that maintain the invariant).
Presentation, problems, discussion.
(2) Temporal Statements and Refinements. Is it claimed that it
is possible to completely avoid certain temporal logic statements and
replace them by refinements of stuttering steps. This raises the
problem of characterizing systems which run forever. Generalization of
"pre, post" pairs.
- Carroll Morgan, Compositionality and "pCSP".
Compositional semantics for probabilistic process algebras have been studied
for decades: one of the major problems is the interaction of the various
forms of choice: probabilistic, internal, external (to use CSP terminology).
What's the new angle?
Work with Annabelle on sequential semantics for probability and demonic
choice has given a logic which is discriminating enough in its observations
to reconstruct the operational (but sequential) program that led to the
observations. The proof of that is not trivial, and (therefore?) the
technique is not much used by other researchers. Yet.
(It is expected values, not new for IFIP2.3...)
Thus we hope it might give us some leverage on this problem. Related
issues turn out to be information hiding and (of course) simulation.
- Werner Dietl, Object Ownership - Overview and Issues
Abstract: I will motivate object ownership and show three concrete systems
that enforce it - two type systems and one dynamic solution. There
should be multiple possible discussion topics, from the basic motivation and
possible applications down to technical problems.
- Alexander Petrenko, Specification Based Testing (SBT): A Practical
The talk will discuss different issues related to SBT technology development
and application. I will involve our case studies for KVEST, UniTesK
and OTK technologies developed and applied in several projects for Nortel
Networks, Microsoft, Intel and other customers. Main points of the
talk are as follows:
- KVEST and UniTesK technologies for test generation from contract
- Roles of models in test suite generation and multiparadigm specifications
in real life applications
- models of: requirements, faults, test coverage,
implementation architecture/structure, behavior (history, trace)
- paradigm combinations: contract specification and FSM/LTS,
- paradigm alternatives in compiler unit testing: contract
specification vs. language specification
- Highest priorities of SBT introduction in practice
- specification without specification language
- how to use formal methods without mathematic background
- SBT vs. conformance testing
- detail vs. simple models and test scenarios
- Rustan Leino, On bounded model checking, induction, and interpolants.
Many interesting state-based computer systems--both software programs and
hardware circuits--can be represented as transition systems. An
execution of a transition system begins in some initial state and then
repeatedly applies a transition relation to obtain the next state. An
important question for such a system is whether or not it is possible for
the system to reach some given set of ``bad'' states. In this
discussion, I consider ways to determine such reachability, trying to
uniformly present previous attempts.
"Test Studio" from Eiffel Software / ETH.
- Karine Arnout
- Eric Hehner
- Doug McIlroy
- Michel Sintzoff
IFIP WG 2.3 home