Vistas in Verified Software

Workshop theme

PLEASE NOTE:

Due to conflicting conferences elsewhere, we have decided to concentrate the 'Tools and experiments for verified software' (VS2W02) workshop activities into the 'From theory to practice' (VS2W01) workshop.

The 'From theory to practice' (VS2W01) workshop title has been updated to 'Vistas in Verified Software' (VS2W01).

Software is playing an increasingly critical role in government, finance, transportation, communication, commerce, and entertainment. Errors in software can have catastrophic consequences leading to loss of life, property, and even identity. Computing theory is crucial to the construction of error-free software through the study of specification and programming languages, and the development of analysis, synthesis, and verification tools and techniques. The workshop features invited talks from distinguished researchers spanning machine learning, distributed systems, concurrency, networking, cyber-physical systems, programming languages, and program analysis.

The goal of the workshop is to identify opportunities where theoretical advances can yield major practical breakthroughs in the construction of verified software.

Applications for this workshop are now closed

Fees

Registration Only

Registration Package: £208
Student Registration Package: £158

The Registration Package includes admission to all seminars, lunches and refreshments on the days that lectures take place (Monday - Friday), wine reception and formal dinner, but does not include other meals or accommodation.

Registration and Accommodation

Accommodation Package: £587

The Accommodation Package includes a registration fee, bed and breakfast accommodation at Churchill College from the evening of Sunday to breakfast on Saturday, together with lunches and refreshments during the days that lectures take place (Monday - Friday). The formal dinner is also included, but no other evening meals

Formal Dinner Only

Formal Dinner: £55

Participants on the Accommodation Package or Registration Package, including organisers and speakers, are automatically included in this event. For all remaining participants who would like to attend, such as programme participants, the above charge will apply.

Accommodation

Accommodation

Accommodation in single study bedrooms with shared facilities and breakfast are provided at Churchill College.

Meals

Lunch Lunch timings and location will be confirmed with timetable.

Evening Meal Participants are free to make their own arrangements for dinner.

Formal Dinner The Formal Dinner location and date is to be confirmed.

Participants on the Accommodation Package or Registration Package, including organisers and speakers, are automatically included in this event.

The Institute kindly requests that any papers published as a result of this programme’s activities are credited as such. Please acknowledge the support of the Institute in your paper using the following text:

The author(s) would like to thank the Isaac Newton Institute for Mathematical Sciences, Cambridge, for support and hospitality during the programme Vistas in Verified Software, where work on this paper was undertaken. This work was supported by EPSRC grant EP/R014604/1.

Timetable

Monday 4th July 2022
09:00 to 09:55	Registration	No Room Required
09:55 to 10:00	Christie Marr Isaac Newton Institute Welcome Talk	No Room Required
10:00 to 11:00	Daniel Kroening University of Oxford TBA	Room 1
11:00 to 11:15	Group Photo and Morning Coffee	No Room Required
11:15 to 12:15	Viktor Kuncak EPFL - Ecole Polytechnique Fédérale de Lausanne Stainless as a Verifying Compiler	Room 1
12:15 to 13:30	Lunch	No Room Required
13:30 to 14:30	Philippa Gardner Imperial College London TBA	Room 1
14:30 to 15:30	David Basin ETH Zürich TBA	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Panel	Room 1
17:00 to 18:00	Welcome Wine Reception at INI	No Room Required

Tuesday 5th July 2022
09:30 to 10:30	Bernhard Möller Universität Augsburg Experiments with Concurrent Kleene Algebra	Room 1
10:30 to 11:00	Group photo and Morning Coffee	No Room Required
11:00 to 12:00	Andrey Rybalchenko Microsoft (UK) Network Verification for Azure Reliability	Room 1
12:00 to 13:30	Lunch	No Room Required
13:30 to 14:30	Mukesh Tiwari University of Cambridge ; Timothy Griffin University of Cambridge; Cambridge Computer Laboratory Extracting a certified OCaml library from Coq.	Room 1
14:30 to 15:30	Moshe Vardi Rice University Program Verification: a 70+-Year History	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Gregory Malecha Bed Rock Systems Verifying a Virtualization Stack at BedRock Systems	Room 1

Wednesday 6th July 2022
09:30 to 10:30	Andrew Appel Princeton University Formally Verifed Numerical Methods	Room 1
10:30 to 11:00	Morning Coffee	No Room Required
11:00 to 12:00	Peter Müller ETH Zürich Verified Secure Routing	Room 1
12:00 to 13:30	Lunch	No Room Required
13:30 to 14:30	Bart Jacobs KU Leuven Abstract nested Hoare triples for modular specification of safety and liveness properties of the I/O behaviour of programs	Room 1
14:30 to 15:30	Sergey Bratus Defense Advanced Research Projects Agency (DARPA) TBA	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Byron Cook Amazon; University College London The business of proof	Room 1
19:30 to 22:00	Formal Dinner at Churchill College	No Room Required

Thursday 7th July 2022
09:30 to 10:30	Dirk Beyer Ludwig-Maximilians-Universität München Cooperative Software Verification: Combination Approaches that Share Information	Room 1
10:30 to 11:00	Morning Coffee	No Room Required
11:00 to 12:00	Cristian Cadar Cadar In Defense of Software Testing & On Techniques for Continuous Testing	Room 1
12:00 to 13:30	Lunch	No Room Required
13:30 to 14:30	Peter Sewell University of Cambridge Wrestling with real systems	Room 1
14:30 to 15:30	Nikhil Swamy Vistas in Proof-oriented Programming: F*, Everest, and Beyond	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Contributed Talks	Room 1

Friday 8th July 2022
09:30 to 10:30	Caterina Urban INRIA Static Analysis for Data Scientists	Room 1
10:30 to 11:00	Morning Coffee	No Room Required
11:00 to 12:00	Mooly Sagiv Tel Aviv University Automatic Detecting Billion $ Coding Errors with Static Program Analysis	Room 1
12:00 to 13:30	Lunch	No Room Required
13:30 to 14:30	Philip Wadler University of Edinburgh Interpreters for Free	Room 1
14:30 to 15:30	Thomas Henzinger IST Austria TBA	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 17:00	Neel Krishnaswami University of Cambridge CN: A separation-logic refinement type system for production systems code verification	Room 1

Saturday 9th July 2022
11:00 to 11:30	Morning Coffee	No Room Required
12:30 to 13:30	Lunch	No Room Required
15:30 to 16:00	Afternoon Tea	No Room Required

Sunday 10th July 2022
11:00 to 11:30	Morning Coffee	No Room Required
12:30 to 13:30	Lunch	No Room Required
15:30 to 16:00	Afternoon Tea	No Room Required

Organisers

Leonardo de Moura Microsoft (UK)
Azadeh Farzan University of Toronto
Philippa Gardner Imperial College London
Kim Larsen Aalborg Universitet
Peter O'Hearn University College London
Natarajan Shankar
Moshe Vardi Rice University

Speakers

Neel Krishnaswami University of Cambridge
Andrey Rybalchenko Microsoft (UK)
Andrew Appel Princeton University
David Basin ETH Zürich
Dirk Beyer Ludwig-Maximilians-Universität München
Sergey Bratus Defense Advanced Research Projects Agency (DARPA)
Cristian Cadar Cadar
Byron Cook Amazon; University College London
Philippa Gardner Imperial College London
Timothy Griffin University of Cambridge; Cambridge Computer Laboratory
Thomas Henzinger IST Austria
Bart Jacobs KU Leuven
Daniel Kroening University of Oxford
Viktor Kuncak EPFL - Ecole Polytechnique Fédérale de Lausanne
Gregory Malecha Bed Rock Systems
Bernhard Möller Universität Augsburg
Peter Müller ETH Zürich
Mooly Sagiv Tel Aviv University
Peter Sewell University of Cambridge
Nikhil Swamy
Mukesh Tiwari University of Cambridge
Caterina Urban INRIA
Moshe Vardi Rice University
Philip Wadler University of Edinburgh

Show All

Participants

Neel Krishnaswami University of Cambridge
Anil Madhavapeddy Cambridge Computer Laboratory
Annabelle McIver Macquarie University
Bill Roscoe University of Oxford
Andrey Rybalchenko Microsoft (UK)
Zhong Shao Yale University
Aws Albarghouthi University of Wisconsin-Madison
Andrew Appel Princeton University
Luca Arnaboldi
David Aspinall University of Edinburgh; The Alan Turing Institute
Anindya Banerjee National Science Foundation
Gilles Barthe Max Planck Institute for Security and Privacy; Max-Planck-Institut für Informatik, Saarbrücken
David Basin ETH Zürich
Mark Batty
Joshua Berdine Facebook Research
Lennart Beringer Princeton University
Dirk Beyer Ludwig-Maximilians-Universität München
Gavin Bierman
Lars Birkedal Aarhus Universitet
Pauline Bolignano
Ahmed Bouajjani Université Paris 7 - Denis-Diderot
Martin Brain City, University of London; University of Oxford
Sergey Bratus Defense Advanced Research Projects Agency (DARPA)
Andrew Butterfield
Cristian Cadar Cadar
Supratik Chakraborty Indian Institute of Technology
Tom Chothia
George Constantinides
Byron Cook University College London
Ugo Dal Lago
Praveen Kumar Dhankar Rashtrasant Tukadoji Maharaj Nagpur University
Brijesh Dongol
Mohamed Elwakil
Daniel Evans University of Illinois at Urbana-Champaign
Uli Fahrenberg
Azadeh Farzan University of Toronto
Kathleen Fisher
Sreepriya G
Philippa Gardner Imperial College London
Timothy Griffin University of Cambridge; Cambridge Computer Laboratory
Thomas Henzinger IST Austria
Warren Hunt University of Texas at Austin
Paul Jackson University of Edinburgh
Bart Jacobs KU Leuven
Jean-Baptiste Jeannin University of Michigan
Cliff Jones Newcastle University
Wolfram Kahl
Sudeep Kanav
Nat Karmios
Katya Komendantskaya
Vasileios Koutavas
Daniel Kroening University of Oxford
Viktor Kuncak EPFL - Ecole Polytechnique Fédérale de Lausanne
Yuhui Lin
Jun Liu
Andreas Loow
Wayne Luk Imperial College London
Petar Maksimovic Imperial College London
Gregory Malecha Bed Rock Systems
Milad Kazemi Mehrabadi None / Other
Ankita Mitra None / Other
Yannick Moy None / Other
Andrzej Murawski
Bernhard Möller Universität Augsburg
Peter Müller ETH Zürich
Daniele Nantes
David Naumann Stevens Institute of Technology
Aditya Nori Microsoft Research - Cambridge
Peter O'Hearn
Steven Obua
Dominic Orchard
Gennaro Parlato
Lawrence Paulson University of Cambridge
Ruzica Piskac Yale University
Andrew Pitts University of Cambridge
Andre Platzer Carnegie Mellon University
Sanjiva Prasad Indian Institute of Technology
Kashish Raimalani
Xiaojia Rao Imperial College London
António Ravara Universidade Nova de Lisboa (UNL)
Alastair Reid
Harald Ruess Fortiss
Mooly Sagiv Tel Aviv University
Karem Sakallah University of Michigan
Daniel Schoepe
Sanjit Seshia University of California, Berkeley
Peter Sewell University of Cambridge
Natarajan Shankar SRI International
William Simmons
Nikhil Swamy
Mukesh Tiwari University of Cambridge
Caterina Urban INRIA
Christian Urban King's College London
Moshe Vardi Rice University
German Vidal
Philip Wadler University of Edinburgh
Conrad Watt University of Cambridge
John Wickerson Imperial College London
Jack Wileden
Glynn Winskel University of Cambridge
James Woodcock University of York; Aarhus Universitet
Shale Xiong ARM
Shale Xiong
Nobuko Yoshida Imperial College London
Naijun Zhan Chinese Academy of Sciences