Meeting 45

Host: Michel Sintzoff
Location: Bruges, Belgium
Dates: 13–17 March 2006

Talks

• Ralph Back, Invariant based programming
• Dines Bjørner
• John R. Harrison, Proving invariants using many-sorted logic
• Peter Henderson
• Tony Hoare, VSTTE conference
  Abstract

  To give a preliminary report on the Conference, and discuss further developments.
• Michael Jackson
• Cliff Jones
• Shriram Krishnamurthi, The Interactive Web
  Abstract

  Web programs are important, increasingly representing the primary public interfaces of commercial organizations. Unfortunately, Web programs also exhibit numerous flaws. In addition to the usual correctness problems faced by software, Web programs must contend with numerous subtle user operations such as clicking the Back button or cloning and submitting a page multiple times. I describe a model checker designed to identify errors in Web software. I present a technique for automatically generating novel models of Web programs from their source code; these models include the additional control flow enabled by these user operations. I exploit a constraint-based approach to avoid over-approximating this control flow; this approach allows us to evade exploding the size of the model.
• Butler W. Lampson
• Gary T. Leavens, Verification by Construction
  Abstract

  In this talk I will present a draft of the research roadmap being worked on by the Verification by Construction subgroup of the Verified Software: Theories, Tools, Experiments conference. Discussions about the recommendations will be welcome.
• K. Rustan M. Leino, Integrated Verification
  Abstract

  In this talk I will present a draft of the research roadmap being worked on by the Integrated Verification subgroup of the Verified Software: Theories, Tools, Experiments conference. Discussions about the recommendations will be welcome.
• Peter Müller, Data Abstraction in Spec# and Boogie
• Tobias Nipkow, A machine-checked proof of the enumeration of tame plane graphs
  Abstract

  Hales' proof of the Kepler conjecture defines a class of tame plane graphs, enumerates that class by computer and checks (again by computer) that none of these graphs constitute a counterexample to the conjecture. This talk reports on the verification of a functional version of Hales' Java program for enumerating tame plane graphs: it is shown that all such graphs are found. This is part of Hales' Flyspeck project to check his whole proof by computer. Throughout the talk we concentrate on the issues that arise when checking mathematical arguments by machine, in particular the challenge of writing programs that are both efficient enough to perform complex searches and enumerations but simple enough that machine-checked correctness proofs become feasible. Joint work with Gertrud Bauer and Paula Schultz.
• J. R. Rao, Recent advances in side-channel cryptanalysis
• Jean-François Raskin, A lattice theory for solving games of imperfect information
  Abstract

  We propose a fixed point theory to solve games of imperfect information. The fixed point theory is defined on the lattice of antichains of sets of states. Contrary to the classical solution proposed by Reif, our new solution does not involve determinization. As a consequence, it is readily applicable to classes of systems that do not admit determinization. Notable examples of such systems are timed and hybrid automata. As an application, we show that the discrete control problem for games of imperfect information defined by rectangular automata is decidable.
• Augusto Sampaio, Test sequence generation from process algebra use models
  Abstract

  My talk will be in the context of a cooperation project between the Federal University of Pernambuco and Motorola. The general purpose of the project is to define a formal strategy for supporting several aspects of software testing. From requirements written in a controlled natural language (with a fixed BNF), the first step is to build a use model represented in CSP. I will concentrate on some initial ideas towards a strategy for automatically generating test sequences direct from the CSP use model. The actual extraction of test sequences is based on refinement checking and can be mechanised using FDR. Joint work with Alexandre Mota and Sidney Nogueira.
• Michel Sintzoff
• Douglas R. Smith, Features/Policies/Aspects: Specification and Enforcement
  Abstract

  The focus of my recent work has been on synthetic techniques for system design by feature composition. I developed a technique for specifying AspectJ-style aspects as logical invariants, and then treating aspect weaving as automatic invariant maintenance (ala Paige's Finite Differencing technique). I also developed an automata-based formalism for specifying features/policies and corresponding enforcement mechanisms based on static analysis.
• Ketil Stølen, STAIRS towards formal design with sequence diagrams
  Abstract

  The STAIRS-method addresses the challenges of harmonizing intuition and formal reasoning. UML interactions (e.g. sequence diagrams) are attractive and intuitive and have been established for years. With the new structuring mechanisms of UML 2.0, they have become more powerful and compact. Our answer lies in a precise understanding of the partial nature of sequence diagrams, and of consistent refinement of such partial understanding to a more complete one.
• Peter Van Roy, Convergence in language design: a case of lightning striking four times in the same place
  Abstract

  What will a definitive programming language look like? I present four case studies of substantial research projects that tackle important problems in four quite different areas: fault-tolerant programming, secure distributed programming, network-transparent distributed programming, and teaching programming as a unified discipline. It turns out that all four languages have a common structure. They can be seen as layered, with the following four layers in this order: a strict functional core, then deterministic concurrency, then message-passing concurrency, and finally shared-state concurrency (usually with transactions). This confirms the importance of functional programming and message passing as important defaults; however, global mutable state is also seen as an essential ingredient.
• Pamela Zave, Toward a discipline of service routing
  Abstract

  This talk introduces basic ideas about what service routing is, why it is not supported by the current Internet architecture, what architectural support might look like, and why it would be valuable to have in the next-generation Internet.