Saturday, 11th February, 2017 @ 9:30 am – 5:00 pm

Introduction to Verification and Testing (INVEST) workshop will take place in the Department of Computing, Imperial College London on Saturday, 11 February 2017. The aim of the workshop is to introduce young researchers, and students potentially interested in research careers, to the fields of software verification and testing. By attending the workshop, you will listen to and engage with world-leading academic scholars, current Post-Docs and PhD students, experience what it’s like being a Verification and Testing researcher, and network with other high achieving participants. 

The workshop will be held in Lecture theatre 340, Huxley building, Department of Computing. The main entrance is at 180 Queen’s Gate. The closest underground station is Gloucester Road, a 10 minute walk.

Agenda

09:30 – 09:55   Registration and Tea and Coffee, Lecture theatre 340, Huxley  building

09:55 – 10:00   Welcome to INVEST 2017

10:00 – 10:50   How to Give Talks That People Can Follow, Derek Dreyer, Max Planck Institute for Software Systems (MPI-SWS), Germany

Some people are naturally gifted speakers, who could command the attention of their audience even if they were reading the ingredients off a box of corn flakes. For the rest of us, preparing a good conference talk is hard work, but it’s not rocket science: the key is to understand how to structure your talk so that your contributions – and why they are important – come through loud and clear. In this talk, I’ll explain the common structural pitfalls that can prevent your audience from following your talk, I’ll present a simple set of concrete principles for avoiding such pitfalls, and I’ll demonstrate how I applied these principles in developing one of my more successful conference talks.

10:50 – 11:10   Break, Tea and Coffee

11:10 – 12:00  Philippa Gardner and Program Specification and Verification Group

• 11:10 Introduction by Philippa Gardner
• 11:20 Petar Maksimovic, An Infrastructure for Tractable Verification of JavaScript Programs

The dynamic nature of JavaScript, together with its complex semantics, makes it a difficult target for symbolic verification techniques. To address this issue, we develop an infrastructure for tractable symbolic verification of JavaScript programs (ECMAScript 5 Strict mode), and present JaVerT, a semi-automatic JavaScript Verification Toolchain built on top of this infrastructure. The infrastructure consists of: (1) JS-2-JSIL, a compiler from JavaScript to JSIL, a simple intermediate goto language suitable for verification; (2) JSIL Verify, a semi-automatic JSIL verification tool based on separation logic; and (3) verified JSIL specifications of JavaScript internal functions. We design JS-2-JSIL to be step-by-step faithful to the ECMAScript standard and systematically test it against the official ECMAScript test suite, passing 100% of the appropriate tests. We provide JSIL reference implementations of the JavaScript internal functions and use JSIL Verify to show that these implementations satisfy their specifications. We demonstrate the feasibility of our verification infrastructure using JaVerT to specify and verify simple JavaScript programs, illustrating our ideas using an implementation of a priority queue. We believe that our infrastructure can be reused for other styles of program analysis for JavaScript.

• 11:40 Gian Ntzik, Reasoning about POSIX File Systems

POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard’s description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. Additionally, the file system is always shared between all available threads and processes, meaning that file-system clients have no control over the interference from the rest of the environment. We provide a formal concurrent specification of POSIX file systems and apply the specification to reason about file-system client programs. Our specifications and reasoning are based on a specification language that combines recent developments in concurrent separation logics with refinement calculus. To reason about file-system clients we introduce specifications conditional on context invariants that restrict the interference from the environment.

12:00 – 12:30   One Minute Madness, Part 1 (attendees present snapshots of their work, 1 minute each)

12:30 – 13:30   Lunch

13:30 – 14:20   Alastair Donaldson  and Multicore Programming Group

• 13:30 Introduction by Alastair Donaldson

• 13:40 Tyler Sorensen, Cooperative Kernels: Multitasking for Blocking Algorithms on GPUs

GPU programming models (e.g. OpenCL) do not mandate fair scheduling, and the (limited) fairness properties provided on current GPUs do not allow for multitasking. Cooperative kernels are a new, simple and powerful programming extension for enabling both intuitive fairness properties *and* multitasking on the GPU. The key idea is that a cooperative kernel can dynamically request more/fewer workgroups based on resource demand from other tasks on the GPU, making this programming model particularly useful for applications with irregular parallelism (such as work-stealing) that use blocking synchronisation. We have a working OpenCL 2.0 prototype and encouraging results showing the feasibility of this approach.

• 14:00 Hugues Evrard, GLFuzz: secure and robust graphics rendering

The rendering of graphics on a dedicated graphics processing units (GPU)  is expressed through programs called “shaders”, which are compiled by the GPU driver. Bugs in shader compilers can lead not only to bad image rendering, but also to more severe issues like system crashes or data leakage. In this talk, we present GLFuzz, a testing framework for OpenGL drivers which relies on metamorphic testing to produce meaningful test cases that isolate driver bugs. GLFuzz has already identified more than 50 driver issues, including system crashes and data leakage, across GPUs of all 7 major vendors (Nvidia, AMD, etc). Beyond OpenGL, GLFuzz can be extended to other shader languages (DirectX, Apple Metal, …), and we are in contact with GPU designers to discuss how GLFuzz could help them deliver more secure and robust drivers.

14:20 – 14:50   One Minute Madness, Part 2

14:50 – 15:10   Break, Tea and Coffee

15:10 – 16:00  Cristian Cadar and Software Reliability Group)

• 15:10  Cristian Cadar, introduction to the Software Reliability Group Symbolic Execution for Evolving Software

One of the distinguishing characteristics of software systems is that they evolve: new patches are committed to software repositories and new versions are released to users on a continuous basis. Unfortunately, many of these changes bring unexpected bugs that break the stability of the system or affect its security. In this talk, I describe some of our work on devising novel symbolic execution techniques for increasing the confidence in evolving software: a technique for reasoning about the correctness of optimisations and refactorings; a technique for high-coverage patch testing, and a technique for revealing behavioural divergences across versions.

• 15:12 Andrea Mattavelli: Constraint Solving in DSE: the Good, the Bad and the Ugly

Dynamic symbolic execution (DSE) is an approach at the core of many modern techniques to software testing, automatic program repair, and reverse engineering. DSE crucially relies on the effectiveness and efficiency of constraint solvers to both explore paths, and generate concrete inputs to exercise the program. In this talk, we present achievements and open challenges of constraint solving in DSE. We also present a set of semantic-preserving transformations to improve the efficiency of constraint solvers in the presence of arrays. We show that our transformations help to improve performance and enable the analysis of code otherwise out of reach for DSE.

• 15:30 Cristian Cadar, Symbolic Execution for Evolving Software

One of the distinguishing characteristics of software systems is that they evolve: new patches are committed to software repositories and new versions are released to users on a continuous basis. Unfortunately, many of these changes bring unexpected bugs that break the stability of the system or affect its security. In this talk, I describe some of our work on devising novel symbolic execution techniques for increasing the confidence in evolving software: a technique for reasoning about the correctness of optimisations and refactorings; a technique for high-coverage patch testing, and a technique for revealing behavioural divergences across versions.

• 15:50 Luis Pina: Deploying Incompatible Analyses in Production through Multi-Version Execution

Dynamic analyses, such as Valgrind and the address/memory compiler sanitizers, are effective at finding and diagnosing challenging bugs and security vulnerabilities. Unfortunately, these powerful analyses cannot be combined and impose high performance overhead. In this talk I will present a FreeDA, a technique based on Multi-Version Execution that allows to deploy several incompatible dynamic analyses in parallel and masks the overhead that such analyses impose for common workloads.

16:00 – 16:45  Discussion

16:45 – Drinks reception

Bios:

Alastair Donaldson is a Senior Lecturer in the Department of Computing, Imperial College London, where he leads the Multicore Programming Group and is Coordinator of the FP7 project CARP: Correct and Efficient Accelerator Programming. He has published more than 50 peer-reviewed papers in formal verification and multicore programming, and leads the GPUVerify project on automatic verification of GPU kernels, which is a collaboration with Microsoft Research. Before joining Imperial, Alastair was a Visiting Researcher at Microsoft Research Redmond, a Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow.

Cristian Cadar is a Reader in the Department of Computing at Imperial College London where he leads the Software Reliability Group and holds an EPSRC Early-Career Fellowship. His research interests span the areas of software engineering, computer systems, and security, with an emphasis on building practical tools for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master’s degrees from the Massachusetts Institute of Technology.

Philippa Gardner is a Professor in the Department of Computing at Imperial College London, and Director of the Research Institute in Automated Program Analysis and Verification funded by GCHQ in association with EPSRC. Her current research focuses on program verification: in particular, reasoning about web programs and reasoning about concurrent programs. She is the leader of the Program Specification and Verification Group at Imperial. She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became Professor in 2009. She is funded by an EPSRC programme grant: `REMS: Rigorous Engineering of Mainstream Systems’ with Cambridge (Sewell, PI) and Edinburgh, and by a GCHQ grant `Certified Verification of Client-side Web Programs’ with Sergio Maffeis at Imperial.

Derek Dreyer heads the Foundations of Programming Group at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany.  His research focuses on building foundations for modular, scalable verification of programs in *realistic* programming languages — languages that combine complex features (e.g. closures, abstract data types, ownership types, weak-memory concurrency) in poorly understood ways.  Toward this end, he has recently been awarded a 2-million-euro Consolidator Grant from the European Research Council for the project RustBelt, concerning the development of rigorous formal foundations for safe systems programming in the Rust language.