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;VALUE=DATE:20141129
DTEND;VALUE=DATE:20141130
DTSTAMP:20260525T190519
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