University of Oxford
Luke Ong is Professor of Computer Science and Director of Graduate Studies, Department of Computer Science, University of Oxford. He read Mathematics and Computer Science at Trinity College, Cambridge and obtained his PhD in Computer Science from Imperial College, London. After a short spell lecturing at the National University of Singapore and a research fellowship at Cambridge, he moved to a University Lectureship at Oxford in 1994. He was promoted to Professor in 2004. Ong has held visiting professorships at Ecole Normale Superieure, Paris, University of Cambridge and National University of Singapore. Ong has contributed to semantics of computation (especially game semantics), types and programming languages, and computational proof theory. A current research focus is automated verification, especially higher-order model checking. He was PC Chair of CSL05, LICS07, FoSSaCS10 and TLCA11; and has served on the council of European Association of Computer Science Logic, and European Joint Conference on Theory and Practice of Software. Ong is General Chair designate of ACM/IEEE Logic in Computer Science.
Title: Verifying Actor-style Message-Passing Concurrency Automatically
Abstract:
The "Actor model" of concurrency organizes computing resources into
independent, sequential communicating processes that share nothing and
communicate by asynchronous message passing. Arguably the gold standard for
concurrency-oriented programming, Erlang is a higher-order functional
programming language that espouses just such a model of concurrency. We
present an approach to verify safety properties of Erlang-style concurrent
programs automatically, by static analysis and infinite-state model checking.
The problem is challenging because Erlang's state space has numerous sources
of un-boundedness. Given an Erlang program, we use a generic and parameterised
control flow analysis to abstract it to an Actor Channel System (ACS), a new
model of channel communication system that accurately captures Erlang's
message passing concurrency. A Turing-powerful model, the ACS is further
approximated by a vector addition system (VAS). The original reachability
problem is then soundly approximated by coverability of the VAS. We have built
a tool called Soter that implements this verification pathway. Despite the
inherent complexity, Soter can verify non-trivial correctness properties of
small but tricky higher-order Erlang programs that spawn an unbounded number
of processes.
Day 2. Gernot Heiser
NICTA and University of New South Wales,
Sydney, Australia
Gernot Heiser is Scientia Professor and John
Lions Chair of Operating Systems at the University of New South Wales (UNSW),
and leads the Software Systems Research Group at NICTA, Australia's National
Centre of Excellence for ICT Research. He joined NICTA at its creation in
2002, and before that was a full-time member of academic staff at UNSW from
1991. His past work included the Mungi single-address-space operating system
(OS), several un-broken records in IPC performance, and the best-ever reported
performance for user-level device drivers. More recently he led the team at
NICTA which produced the world's first formal proof of functional correctness
of a protected general-purpose operating-system kernel, the first complete and
sound worst-case execution time analysis of a protected OS kernel, and the
synthesis of high-performance device drivers.
In 2006, Gernot with a number of his students founded Open Kernel Labs, now
the market leader in secure virtualization technology for embedded systems.
The company's OKL4 operating system, a descendent of L4 kernels developed by
his group at UNSW and NICTA, is deployed in more than 1.5 billion mobile
devices. This includes the Motorola Evoke, the first (and to date only) mobile
phone running a high-level OS (Linux) and a modem stack on the same processor
core.
In a former life, Gernot developed semiconductor device simulators and models
of device physics for such simulators, and pioneered the use of
three-dimensional device simulation for the characterisation an optimisation
of high-performance silicon solar cells.
Title of talk: A Platform for Trustworthy Systems
Abstract: Safety and security of computing systems is becoming an increasing challenge, as their complexity increases while at the same time they are increasingly trusted with critical functions. This talk provides an overview of the Trustworthy Systems activities at NICTA, which aim to provide a platform that can support real-world systems and allows us to make strong guarantees about their safety, security or reliability. The approach is based on the large-scale application of theorem proving and other formal methods. It has resulted in the design and implementation of a microkernel, called seL4, with a proof of functional correctness and integrity enforcement as well as a sound and complete worst-case timing model. Secure-system prototypes using this kernel have been demonstrated and analyzed. Present work, besides proving further security properties of the kernel, focuses on a framework supporting the construction of provably trustworthy systems which include large, un-trusted legacy components.
Microsoft Research India, Bangalore
G. Ramalingam is a Principal Researcher at Microsoft Research India. He received his B. Tech from IIT Madras and his Ph.D. from the University of Wisconsin-Madison. He was previously a researcher at IBM T. J. Watson Research Center from 1993 to 2006. His research interests are in the area of Programming Languages and Tools, with a particular interest in Static Program Analysis, Program Understanding, Software Verification, Concurrency and Distributed Systems. He is the recipient of the President's Gold Medal (at IIT Madras), an IBM Outstanding Technical Achievement award, and is an ACM Distinguished Scientist.
Title:
Failure-Free Computation Via Idempotence
Abstract:
Writing applications against modern distributed storage platforms is
challenging because of the pitfalls of distribution such as process failures,
imperfect messaging, shared mutable state, and logical failures (exceptions).
In this talk, we introduce a simple core language that formalizes notions of
process failure, a default recovery mechanism, data partitioning, local atomic
transactions that are restricted to a single store, and message duplication.
We formalize a generic correctness criterion, namely failure-freedom, for
applications written in this language, focusing on their ability to tolerate
process failures and message duplication. Idempotence is a key property for
achieving failure-freedom. We describe an efficient (monad-based)
implementation that automatically guarantees idempotence and fail-free
computations without requiring distributed coordination. We then generalize
this idea into a new language primitive for specifying fail-free computations.
We finally consider logical failures and introduce an enriched language
construct called molecular transactions. A molecular transaction is a
fail-free composition of atomic transactions with user-defined compensating
actions.
