MEMOCODE'14

Joseph Sifakis,
Turing Award
EPFL

System Design - Challenges and Work Directions
Modern computing systems break with traditional systems, such as desktop computers and servers, in various ways: 1) they are instrumented in order to interact with physical environments; 2) they are interconnected to allow interaction between people and objects in entirely new modes; 3) they must be smart to ensure predictability of events and optimal use of resources. Currently, we lack theory methods and tools for building cost-effectively trustworthy systems.
In this talk, I will discuss system design as a formal and accountable process leading from requirements to correct-by-construction implementations. I will also discuss current limitations of the state of the art and advocate a coherent scientific foundation for system design by presenting a vision raising three grand challenges: 1) linking the cyber and the physical worlds; 2) correct component-based construction; 3) intelligence.
I will conclude with general remarks about the nature of computing and advocate a deeper interaction and cross-fertilization with other more mature scientific disciplines.

Wayne Burleson
University of Massachusetts at Amherst

Security and privacy in implantable medical devices: an ongoing concern
In the last 5 years, there has been a considerable increase in research and awareness of security and privacy issues in implantable medical devices. This has been driven by the rapid introduction and deployment of an increasing diversity of medical devices. Although wearable and clinical devices are also of interest, the implantable nature of many recent devices significantly increases risks as well as engineering challenges. This talk will use several case studies to review the multi-disciplinary process in which vulnerabilities are analyzed, disclosed, and repaired. Business incentives and regulations play an important role in the overall process.
Technical challenges include energy harvesting, side-channel protection, lightweight crypto, personalization, wireless communications, security/safety tradeoffs, and human factors. Several open research areas will be discussed.

Bertrand Meyer
ETH Zurich and Eiffel Software

Proving (and revisiting) what programs do not
In 2007, I had the honor of an invited presentation at MEMOCODE, where I discussed the frame problem: how to establish that programs do *not* modify certain properties. The problem is particularly challenging in the case of object-oriented programs involving complex pointer (reference) data structures. Seven years later, it is still largely an open problem, although significant progress has occurred. After realizing that a satisfactory solution requires addressing another difficult problem, alias analysis, I have devoted much of my work to program analysis techniques that tackle both aliasing and framing. Taking advantage of the kind invitation to present again at MEMOCODE, I will describe the current state of this work and how its results are embodied in program analysis tools that provide automatic means -- not requiring program annotations -- to ascertain fundamental properties of programs.

Johannes Kinder
Royal Holloway, University of London

Efficient symbolic execution for software testing
Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. While the basic technique had been introduced already in the 70s, the advent of modern SAT and SMT solvers has lead to a surge of tools and techniques in the area over the last decade. This tutorial will introduce and compare the different approaches to using symbolic execution for testing and discuss the specific challenges and trade-offs. A main challenge in symbolic execution is path explosion, and various proposals have been made to either combat it. I will discuss how these techniques affect the number and type of solver queries that have to be made, and how this can lead to surprising effects on the efficiency of a symbolic execution engine. Going further, we will look at developments to increase the scope of symbolic execution to larger software systems. Specific topics covered include state merging, procedure summaries, abstraction, search strategies, and parallelization.

Armin Biere
Johannes Kepler University, Linz

Challenges in Bit-Precise Reasoning
Bit-precise reasoning (BPR) precisely captures the semantics of systems down to each individual bit and thus is essential to many verification and synthesis tasks for both hardware and software systems. As an instance of Satisfiabiliy Modulo Theories (SMT), BPR is in essence about word-level decision procedures for the theory of bit-vectors. In practice, quantiers and other theory extensions, such as reasoning about arrays, are important too. In the first part of the tutorial we gave a brief overview on basic techniques for bit-precise reasoning and then covered more recent theoretical results, including complexity classification results. We discussed challenges in developing an efficient SMT solver for bit-vectors, like our award winning SMT solver Boolector, and in particular presented examples, for which current techniques fail. Finally, we reviewed the state-of-the-art in word-level model checking, and argued why it is necessary to put more effort in this direction of research.

A short video about Lausanne

Conference location on Google

An interactive map of EPFL