Introduction to Verification and Testing (INVEST) workshop will take place in the Department of Computing, Imperial College London on Saturday, November 29 2014. 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.
Who should attend
Outstanding computer science undergraduate students in their third or final year/postgraduate students/early stage PhD students. We expect most of the attendees to come from the UK/Europe (no assistance related to UK visa can be provided).
How to apply
The decisions on accepting participants would be made on a case by case basis.
There is no charge for the workshop. Complimentary tea, coffee and lunch will be provided, but participants are expected to make their own travel and accommodation arrangements.
Important dates
Application deadline: Fri, Nov 14, 2014
Notification of application status: Mon, Nov 17, 2014
Workshop: Sat, Nov 29, 2014
Agenda
09:15 – 09:30 Registration
09:30 – 09:35 “Overview of research activities of the Multicore group”, Alastair Donaldson
09:35 – 10:30 “Automated verification of GPU kernels”, Nathan Chong
10:30 – 10:45 Break
10:45 – 11:00 “Introduction to the Software Reliability Group”, Cristian Cadar
11:00 – 11:45 “Dynamic Symbolic Execution”, Cristian Cadar
11:45 – 12:00 Break
12:00 – 12:30 “Reasoning about Higher-order JavaScript”, Philippa Gardner
12:30 – 13:00 “Towards Tractable Verification of JavaScript Programs”, Daiva Naudziuniene
13:00 – 14:00 Lunch
14:00 – 14:40 “Systematic testing for concurrent software”, Paul Thomson
14:40 – 15:00 “Fuzz testing compilers for a heterogeneous many-core language”, Alastair Donaldson
15:00 – 15:15 Break
15:15 – 15:30 “Finding Data Races in GPU Kernels Using Symbolic Execution”, Dan Liew
15:30 – 15:52 “Toward Generic Automatic Document Recovery”, Tomasz Kuchta
15:52 – 16:15 “Efficient N-version Execution: Because More is Better”, Petr Hosek
16:15 – 16:30 Break
16:30 – 17:00 “Introduction to reasoning about concurrent programs”, Philippa Gardner
17:00 – 17:30 “CoLoSL-Compositionality At Last!”, Azalea Raad
17:30 – 18:00 Discussion
Abstracts
“Practical Verification Techniques for Multicore Software”, Alastair Donaldson
Over two sessions, I will give an overview of the research activities being undertaken in the Multicore Programming Group. The sessions will be interactive, featuring demonstrations of our analysis tools by members of my group as well as technical slides on the methods underlying our work.
The first session will be devoted to our GPUVerify project, a technique and tool for static verification of software that has been designed for acceleration on graphics processing units (GPUs). At the heart of this approach is a method for reducing the problem of verifying a massively parallel GPU kernel to the task of verifying a sequential program. I will provide an overview of this method, and explain how the resulting sequential verification task can be attacked using verification condition generation and theorem proving.
In the second session I will cover very recent work by the group on stateless model checking for concurrent Java programs, and on validation techniques for many-core compilers.
“Practical techniques and tools for improving the reliability and security of real-world software”, Cristian Cadar
Over two sessions, my group and I will give an overview of the current research of the Software Reliability Group at Imperial College London.
Our research focuses on building practical techniques and tools for improving the reliability and security of real-world software. Ongoing projects include techniques for comprehensively testing software patches, finding bugs in code running on GPUs, surviving errors in software updates, and recovering documents that crash or fail to load correctly.
“Modular Reasoning about Programs”, Philippa Gardner
My group focusses on theory and tools based on modular reasoning about programs using separation logic: in particular, reasoning about web programs and concurrent programs.
We will give an overview of the current work being done by the group: one session on JavaScript; the other on concurrency. Our research includes: reasoning about JavaScript programs (such as code from the game 2048); foundational reasoning about shared-memory concurrent algorithms; and specifying libraries (java.util.concurrent, DOM and POSIX) and reasoning about client programs which use these libraries.
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 Senior Lecturer in the Department of Computing at Imperial College London where he leads the Software Reliability Group (http://srg.doc.ic.ac.uk) 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 and Director of the Research Institute in Automated Program Analysis and Verification, funded by GCHQ in association with EPSRC. She completed her PhD thesis, supervised by Professor Gordon Plotkin at Edinburgh in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial. She is funded by two EPSRC programme grants: `Resource Reasoning’ with UCL (O’Hearn and then Pym, PI) and Oxford, and `REMS: Rigorous Engineering of Mainstream Systems’ with Cambridge (Sewell, PI) and Edinburgh, and by GCHQ grant `Certified Verification of Client-side Web Programs’ with Sergio Maffeis at Imperial.