BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Research Cluster in Verification and Testing - ECPv6.15.11//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Research Cluster in Verification and Testing
X-ORIGINAL-URL:http://wp.doc.ic.ac.uk/verificationgroup
X-WR-CALDESC:Events for Research Cluster in Verification and Testing
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20130101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20170211T093000
DTEND;TZID=UTC:20170211T170000
DTSTAMP:20260518T052034
CREATED:20170111T130559Z
LAST-MODIFIED:20170209T173033Z
UID:133-1486805400-1486832400@wp.doc.ic.ac.uk
SUMMARY:Workshop – Introduction to Verification and Testing (INVEST)\, 2017
DESCRIPTION:Saturday\, 11th February\, 2017 @ 9:30 am – 5:00 pm \nIntroduction 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.  \nThe 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. \nAgenda \n09:30 – 09:55   Registration and Tea and Coffee\, Lecture theatre 340\, Huxley  building \n09:55 – 10:00   Welcome to INVEST 2017 \n10:00 – 10:50   How to Give Talks That People Can Follow\, Derek Dreyer\, Max Planck Institute for Software Systems (MPI-SWS)\, Germany \nSome 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. \n10:50 – 11:10   Break\, Tea and Coffee \n11:10 – 12:00  Philippa Gardner and Program Specification and Verification Group \n\n11:10 Introduction by Philippa Gardner\n11:20 Petar Maksimovic\, An Infrastructure for Tractable Verification of JavaScript Programs\n\nThe 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. \n\n11:40 Gian Ntzik\, Reasoning about POSIX File Systems\n\nPOSIX 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. \n12:00 – 12:30   One Minute Madness\, Part 1 (attendees present snapshots of their work\, 1 minute each) \n12:30 – 13:30   Lunch \n13:30 – 14:20   Alastair Donaldson  and Multicore Programming Group \n\n13:30 Introduction by Alastair Donaldson\n\n\n13:40 Tyler Sorensen\, Cooperative Kernels: Multitasking for Blocking Algorithms on GPUs\n\nGPU 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. \n\n14:00 Hugues Evrard\, GLFuzz: secure and robust graphics rendering\n\nThe 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. \n14:20 – 14:50   One Minute Madness\, Part 2 \n14:50 – 15:10   Break\, Tea and Coffee \n15:10 – 16:00  Cristian Cadar and Software Reliability Group) \n\n15:10  Cristian Cadar\, introduction to the Software Reliability Group Symbolic Execution for Evolving Software\n\nOne 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. \n\n15:12 Andrea Mattavelli: Constraint Solving in DSE: the Good\, the Bad and the Ugly\n\nDynamic 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. \n\n15:30 Cristian Cadar\, Symbolic Execution for Evolving Software\n\nOne 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. \n\n15:50 Luis Pina: Deploying Incompatible Analyses in Production through Multi-Version Execution\n\nDynamic 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. \n16:00 – 16:45  Discussion \n16:45 – Drinks reception \nBios: \nAlastair 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. \nCristian 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. \nPhilippa 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. \nDerek 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.
URL:http://wp.doc.ic.ac.uk/verificationgroup/event/workshop-introduction-to-verification-and-testing-invest-2017/
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=UTC:20151205T093000
DTEND;TZID=UTC:20151205T173000
DTSTAMP:20260518T052034
CREATED:20151019T110509Z
LAST-MODIFIED:20151214T101126Z
UID:121-1449307800-1449336600@wp.doc.ic.ac.uk
SUMMARY:Workshop - Introduction to Verification and Testing (INVEST)\, 2015
DESCRIPTION:Introduction to Verification and Testing (INVEST) workshop will take place in the Department of Computing\, Imperial College London on Saturday\, December 5 2015. 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. \nWho should attend\nOutstanding 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). \nHow to apply\nTo be considered for a place on the workshop\, please send an email (see Contact us page) providing your name\, the name of your PhD supervisor or tutor\, the name of your university\, and a brief statement on why you want to attend this workshop. \nThe decisions on accepting participants would be made on a case by case basis. \nThere 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. \nImportant dates\nApplication deadline: Mon\, Nov 30\, 2015 \nNotification of application status: Wed\, Dec 2\, 2015 \nWorkshop: Sat\, Dec 5\, 2015 \nAgenda\n09:30 – 09:50   Registration and Coffee \n09:50 – 09:55   Welcome to INVEST 2015 \n09:55 – 10:35   Symbolic Execution for Evolving Software\, Cristian Cadar (Software Reliability Group) \n10:35 – 10:45   Break \n10:45 – 11:35   Understanding and Verifying JavaScript Programs\, Philippa Gardner (Resource Reasoning Group) \n11:35 – 11:45   Break \n11:45 – 12:15   Metamorphic Compiler Testing\, Alastair Donaldson (Multicore Programming Group) \n12:15 – 12:30   On Broken Documents and Automatic Document Recovery\, Tomasz Kuchta (Software Reliability Group) \n12:30 – 13:00   One Minute Madness\, part 1 (attendees present snapshots of their work\, 1 minute each) \n13:00 – 14:00   Lunch and Coffee \n14:00 – 14:20   Analysing Asynchronous Concurrent Programs with the P# Language\, Pantazis Deligiannis (Multicore Programming Group) \n14:20 – 14:35   Towards Deployment-Time Dynamic Analysis of Server Applications\, Luis Pina (Software Reliability Group) \n14:35 – 15:00   One Minute Madness\, part 2 (attendees present snapshots of their work\, 1 minute each) \n15:00 – 15:10   Break \n15:10 – 15:25   Symbooglix: A Symbolic Execution Engine for Boogie Programs\, Dan Liew (Multicore Programming Group and Software Reliability Group) \n15:25 – 15:45   Concurrency and Termination Verification\, Julian Sutherland (Resource Reasoning Group) \n15:45 – 16:05   An Empirical Investigation of GPU Memory Consistency\, Tyler Sorensen (Multicore Programming Group) \n16:05 – 16:15   Break \n16:15 – 17:00   How to Do a Bad (or Good) PhD and How to Give a Bad (or Good) Talk\, Cristian Cadar (Software Reliability Group) \n17:00 – 17:30   Discussion \n\nBios:\nAlastair 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. \nCristian Cadar is a Reader 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. \nPhilippa 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. \n 
URL:http://wp.doc.ic.ac.uk/verificationgroup/event/workshop-introduction-to-verification-and-testing-invest-2015/
END:VEVENT
BEGIN:VEVENT
DTSTART;VALUE=DATE:20141129
DTEND;VALUE=DATE:20141130
DTSTAMP:20260518T052034
CREATED:20140826T113426Z
LAST-MODIFIED:20151214T101019Z
UID:82-1417219200-1417305599@wp.doc.ic.ac.uk
SUMMARY:Workshop - Introduction to Verification and Testing (INVEST)
DESCRIPTION: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. \nWho should attend\nOutstanding 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). \nHow to apply\nThe decisions on accepting participants would be made on a case by case basis. \nThere 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. \nImportant dates\nApplication deadline: Fri\, Nov 14\, 2014 \nNotification of application status: Mon\, Nov 17\, 2014 \nWorkshop: Sat\, Nov 29\, 2014 \nAgenda\n09:15 – 09:30   Registration \n09:30 – 09:35   “Overview of research activities of the Multicore group”\, Alastair Donaldson \n09:35 – 10:30   “Automated verification of GPU kernels”\, Nathan Chong \n10:30 – 10:45    Break \n10:45 – 11:00    “Introduction to the Software Reliability Group”\, Cristian Cadar \n11:00 – 11:45    “Dynamic Symbolic Execution”\, Cristian Cadar \n11:45 – 12:00    Break \n12:00 – 12:30    “Reasoning about Higher-order JavaScript”\, Philippa Gardner \n12:30 – 13:00    “Towards Tractable Verification of JavaScript Programs”\, Daiva Naudziuniene \n13:00 – 14:00    Lunch \n14:00 – 14:40    “Systematic testing for concurrent software”\, Paul Thomson \n14:40 – 15:00    “Fuzz testing compilers for a heterogeneous many-core language”\, Alastair Donaldson \n15:00 – 15:15    Break \n15:15 – 15:30    “Finding Data Races in GPU Kernels Using Symbolic Execution”\, Dan Liew \n15:30 – 15:52    “Toward Generic Automatic Document Recovery”\, Tomasz Kuchta \n15:52 – 16:15    “Efficient N-version Execution: Because More is Better”\, Petr Hosek \n16:15 – 16:30    Break \n16:30 – 17:00    “Introduction to reasoning about concurrent programs”\, Philippa Gardner \n17:00 – 17:30    “CoLoSL-Compositionality At Last!”\, Azalea Raad \n17:30 – 18:00    Discussion \n  \nAbstracts\n“Practical Verification Techniques for Multicore Software”\, Alastair Donaldson \nOver 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. \nThe 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. \nIn 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. \n“Practical techniques and tools for improving the reliability and security of real-world software”\, Cristian Cadar \nOver two sessions\, my group and I will give an overview of the current research of the Software Reliability Group at Imperial College London. \nOur 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. \n“Modular Reasoning about Programs”\, Philippa Gardner \nMy group focusses on theory and tools based on modular reasoning about programs using separation logic: in particular\, reasoning about web programs and concurrent programs. \nWe 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. \n\nBios:\nAlastair 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. \nCristian 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. \nPhilippa 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. \n 
URL:http://wp.doc.ic.ac.uk/verificationgroup/event/workshop-introduction-to-verification-and-testing-invest-2014/
LOCATION:Huxley Building\, Imperial College London
END:VEVENT
END:VCALENDAR