Invited Talks

Using Kilim's Isolation Types for Multicore Efficiency

Alan Mycroft, Cambridge University

We identify a `memory isolation' property which enables multi-core programs to avoid slowdown due to cache contention. We give a tutorial on existing work on Kilim and its isolation-type system building bridges with both substructural types and memory isolation.






The Practical Application of Formal Methods:

Where is the Benefit for Industry?
James J. Hunt, aicas incorporated

Though the use of formal methods for software verification has progress tremendously in the last ten year, its take up in industry has been meager, but with the right emphasis this could change dramatically.  Software certification standards have started to take  formal methods seriously as an alternative to testing.  By focusing on practical issues such as common specification languages, adaption to industrial processes for safety certification, scalability, training, and synergies between tools, common reservations about using formal methods could be lain to rest.  This could help formal methods become  the center of software engineering in the coming decade.





Local Reasoning for Verification of Object-based Programs Using First-order Assertions
Anindya Banerjee, IMDEA Software

Shared mutable objects pose challenges in reasoning, especially for
data abstraction and modularity. We present a logic for
error-avoiding partial correctness of programs featuring shared
mutable objects. Using a first order assertion language, the logic
provides heap-local reasoning about mutation and separation, via ghost
fields and variables of type "region" (finite sets of object
references). We show the logic in use in proving the correctness of the
composite design pattern. We also show how the logic can be used to
reason about the hiding of internal invariants in a procedure specification
and how to perform client reasoning in a manner that does not invalidate
the internal invariants.

Joint work with David A. Naumann and Stan Rosenberg (Stevens Institute
of Technology).

Modelling Distributed Adaptable Object Oriented Systems using HATS Approach:

A Fredhopper Case Study

Peter Wong, Fredhopper

The HATS project aims at developing a model-centric methodology for the design, the implementation and the verification of distributed, concurrent and highly configurable systems. Such systems also have high demands on their dependability and trustworthiness. The HATS approach is centered around the Abstract Behavioural Specification modelling language (ABS) and its accompanying tools suite. The HATS approach allows precisely specifying and analyzing the abstract behaviour of distributed software systems and their spatial and temporal variability. The HATS project measures its success by applying its framework not only to toy examples, but to real industrial scenarios.

In this talk, we consider the HATS approach for modelling an industrial scale case study provided by the eCommerce company Fredhopper. In this case study we consider Fredhopper Access Server (FAS). We show how to model the commonality and variability of FAS's replication system using ABS and discuss our experience.