In the Leonardo project we explore an alternative way of organizing the central software of computers whereby the redundant duplication of concepts and facilities should be greatly reduced. The kernel of the new system inherits traits from both operating system shells, programming language systems, discrete simulation systems, knowledge-based agent systems and others. It integrates a number of facilities that are usually considered as peripheral, such as an ontology structure and a version management facility. Facilities for communication between multiple such agent-like systems for the purpose of task-sharing and information exchange is an essential ingredient in the design.

In the talk I will briefly describe the present, experimental implementation and then discuss the project from the following points of view: - Short-term and long-term opportunities for major reform of computer software architecture - Discussion of what types of software systems can with advantage be assimilated into a comprehensive architecture, with particular emphasis on human-robot dialog systems in multi-robot environments - Perspective on textual data languages, such as XML and OWL, as compared with the representation developed in Leonardo - New aspects on logics of actions and change that are obtained when working with the actual system implementation.

It is widely acknowledged that today's network management tools are inadequate. Although the existing managment protocol (SNMP) has been and remains indispensible, it offers neither the scalability nor the functionality needed to manage large systems. Active/programmable networks and mobile agent systems have been proposed as alternative network management solutions that offer more functionality and potentially better scalability. Unfortunately, the flexibility of these (heavyweight) approaches comes with its own set of problems which prevent them from being widely adopted.

This talk will describe the use of ephemeral state processing (ESP) to efficiently monitor and collect information from large networks. ESP is a lightweight router-based programmable building block that can solve a range of network management problems while avoiding the problems that plague more complex approaches. Moreover, the simplicity of ESP allows it to be made available as a general-purpose service for all packets in the network. We demonstrate the utility of the service by showing how it can be used to solve some common network management problems.

(Joint work with J. Griffioen)

The concept of "design pattern" is well known in Object Oriented Technology. The main idea is to have some sort of reproducible engineering micro-design that the software designer can use in order to develop new pieces of software. In this presentation, I try to borrow such OO ideas and incorporate them within the realm of formal methods.

First, I will proceed by defining (and prove) two formal patterns, where the second one happens to be a refinement of the first one. As a matter of fact, one very often encounters such patterns in the development of reactive systems, where several chains of reactions can take place between an environment and a software controller, and vice-versa.

Second, the patterns are then used many times in the development of a complete reactive system where several pieces of equipment interact with a software controller. It results in a systematic construction made of six refinements. The entire system is proved completely automatically.

The relationship between the formal design patterns and the formal development of the problem at hand will be shown to correspond to a certain form of refinement. A demo will be shown.

Hanging chads, among other issues with traditional voting systems, have sparked great interest in managing the election process through the use of newer electronic voting systems. While computer scientists, for the most part, have been warning of the perils of such action, vendors have forged ahead with their products, claiming increased security, reliability, and accuracy. Many municipalities have adopted electronic systems and the number of deployed systems is rising. To the limited extent that independent security analyses have been published, the results have raised serious reservations about the quality of these systems to resist attacks. This talk will describe problems we and other researchers have discovered and will consider the limitations of the certification processes that should have guaranteed some quality control. These issues, in turn, give rise to a variety of interesting research problems that span computer science, human factors, and public policy. In this talk, we will consider how both established and open research in software engineering, distributed systems, and cryptography can and should impact the next generation of voting systems.

Adaptive Embedded Systems While embedded systems are ubiquitous, adaptive ones are not. My research goal is to push the science and engineering of adaptive embedded systems by exploring the addition of adaptivity to a diverse variety of complex systems. I will present my work on four current projects (1) tracking human learning on a complex visual-motor task (2) predicting conflict from events data extracted from wire stories (3) customizing application-specific compiler optimization sequences, and (4) learning regulatory networks in normal and cancer cells.

Computer systems should be trustworthy in the sense that they should reliably answer requests from legitimate users and protect confidential information from unauthorized users. Building this kind of systems is challenging, even more so in the increasingly common case where control is split between multiple administrative domains.

Byzantine fault tolerance techniques can elegantly provide reliability without overly increasing the complexity of the system and have recently earned the attention of the system community. In the first part this talk I discuss some of the contributions I have made toward practical Byzantine fault tolerance---in particular, how to reduce the cost of replication and how to reconcile replication with confidentiality. In the second part of the talk I argue that Byzantine fault-tolerance alone is not sufficient to deal with cooperative services under multiple administrative domain, where nodes may deviate from their specification not just because they are broken or compromised, but also because they are selfish. To address this challenge, I propose BAR, a new failure model that combines concepts from Byzantine fault-tolerance and Game Theory. I will describe BAR, present an architecture for building BAR services, and briefly discuss BAR-B, a BAR-tolerant cooperative backup system.

We present a new approach for statically analyzing data structure consistency properties. Our approach is based on specifying interfaces of data structures using abstract sets and relations.This enables our system to independently verify that

1) each data structure satisfies internal consistency properties and each data structure operation conforms to its interface;

2) the application uses each data structure interface correctly, and maintains the desired global consistency properties that cut across multiple data structures.

Our system verifies these properties by combining static analyses, constraint solving algorithms, and theorem provers, promising an unprecedented combination of precision and scalability. The combination of different techniques is possible because all system components use a common specification language based on sets and relations.

In the context of our system, we developed new algorithms for computing loop invariants, new techniques for reasoning about sets and their sizes, and new approaches for extending the applicability of existing reasoning techniques. We successfully used our system to verify data structure consistency properties of examples based on computer games, web servers, and numerical simulations. We have verified implementations and uses of data structures such as linked lists with back pointers and iterators, trees with parent pointers, two-level skip lists, array-based data structures, as well as combinations of these data structures. This talk presents our experience in developing the system and using the system to build verified software.

Large software systems consist of dozens and hundreds of interlocking components. Software engineers adapt components from other suppliers, create their own, and glue all of these together in one large product. In this world, it becomes critical to pinpoint flaws quickly when software fails. Then the component consumer can request a fix from the producer of the faulty component or replace the component with an equivalent component from a different producer.

To get to this world, programmers must learn to use interfaces and to enrich them with contractual specifications. Programming language researchers must explore interface-oriented programming in its most radical form and must evaluate its pragmatic consequences. In this talk, I report on our first steps in this direction, presenting empirical findings, research results, research plans, and wild speculations.

As the Internet is a human designed system one should have full knowledge about its operations and how it is used. Yet this is not the case as it is a prime example of a complex distributed software system that is managed in a decentral manner. With regards to how the Internet is managed I will present how to extract an inter-domain topology model that captures the route diversity of the Internet. With regards to how the Internet is used and abused by its users I will present extensions to an network intrusion detection system that enable us to perform dynamic application-layer protocol analysis and show how a time machine can be used for security forensics and network trouble-shooting.

Systems Biology is a new discipline aiming to understand the behavior of biological systems as it results from the (non-trivial, "emergent") interaction of biological components. We discuss some biological networks that are characterized by simple components, but by complex interactions. The components are separately described in stochastic pi-calculus, which is a "programming language" that should scale up to description of large systems. The components are then wired together, and their interactions are studied by stochastic simulation. Subtle and unexpected behavior emerges even from simple circuits, and yet stable behavior emerges too, giving some hints about what may be critical and what may be irrelevant in the organization of biological networks.

Spec# is a programming system that aims to provide programmers with a higher degree of rigor than in common languages today. The Spec# language extends the object-oriented .NET language C#, adding features like non-null types, pre- and postconditions, and object invariants. In addition to static type checking and compiler-emitted run-time checks for specifications, Spec# has a static program verifier. The program verifier translates Spec# programs into verification conditions, which are then analyzed by an automatic theorem prover. In this talk, I will give an overview of Spec#, including a demo. I will then discuss some aspects of its design in more detail.

Developing correct multithreaded software is very challenging, due to the potential for unintended interference between threads. We present type systems for verifying two key non-interference properties in multithreaded software: race-freedom and atomicity. Verifying atomicity is particularly valuable since atomic procedures can be understood according to their sequential semantics, which significantly simplifies subsequent (formal and informal) correctness arguments. We will describe our experience applying these type systems and corresponding type inference algorithms to standard multithreaded benchmarks and other applications, and illustrate some defects revealed by this approach.

Computing and communication devices are pervasively embedded into our everyday environments. Interaction in the context of the real world includes more and more interacting with complex mobile and embedded information systems. In many cases such interaction is multimodal and distributed between public and personal mobile devices. Advances in underlying network, processing, perception, and actuation technologies as well as new production techniques, such as 3D-printing, allow unprecedented options for creating novel user interfaces. However, as constraints that applied to the domain of mechanical and electrical user interfaces are not given anymore, there is a great risk of creating user interfaces where the conceptual model is not understandable anymore. To make pervasive computing usable, establishing appropriate interaction paradigms and metaphors is the great challenge.

Context-Aware Interaction, Implicit Interaction and Tangible User Interfaces are novel approaches which take into account that the interaction with information happens in the real world and is conceptually embedded into foreground tasks carried out by the user. To explore opportunities and challenges several prototypical systems were designed, implemented, and evaluated. Using case studies the talk presents innovative mobile phone applications that make use of contextual information, novel interactive devices, and conventional objects and computers that are enriched by pervasive technologies. This will outline the interplay between pervasive technologies, mobile systems and user experience.

Concentrating on what information is created and what information is consumed by the user while performing a task in the real world is the basic idea of Embedded Interaction. The focus is not on a single technology or a specific device. The aim is to seek optimal support for a task considering all technologies available in a certain context. This requires an understanding of different parameters of novel input and output technologies. The talk concludes with an outlook on research challenges that arise from the concept of Embedded Interaction related to current developments in the field of pervasive computing.