Programme theme
Computer software plays an increasingly critical role in our lives. We trust software to drive cars, fly airplanes, control air traffic, perform surgery, monitor nuclear power plants, execute financial transactions, among other things.These applications run on a software stack that provides the functionality for regulating access to hardware devices, communicating over the network, managing files, compiling code, and running applications. On the one hand, the modern software stack is a profound engineering achievement. With a few keystrokes, we can execute tasks that require billions of tightly coordinated steps for sending an email or browsing a web page. On the other hand, even a small error in a program in the software stack can leak private data, allow unauthorized access, disrupt air traffic, or corrupt or delete valuable information. The threats posed by incorrect software provoke the following questions:
How do we construct software stacks with accurate mathematical models and provably predictable behavior
relative to these models?
Can we build mathematical models and proofs for verifying safety and security properties of complex software systems that operate cars and planes and manage financial transactions?
What theoretical advances are needed for modeling and analysing large software systems?
What language and semantic analysis tools can assist in the large-scale construction of verified software?
Can we create an ecosystem of high-quality verified software with well-defined interfaces and composition mechanisms?
The six week program on Verified Software at the Isaac Newton Institute brings together a diverse mix of researchers for the purpose of identifying the theoretical and practical challenges in algorithmic verification, synthesis, and certification of software systems; designing new languages, formalisms, tools, and integrated tool suites for the modeling and analysis of complex systems; identifying novel applications and challenge problems for verification technology; and crafting a roadmap for research, education, and technology. The Verified Software programme includes two workshops, one on the Theory and Applications of Verified Software, and a second one on Verification Tools and Experiments. These will be supplemented with smaller workshops and working groups devoted to specialized topics and industrial applications. The Isaac Newton Institute programme on Verified Software offers an opportunity to take stock of the first fifteen years of Tony Hoare’s Verified Software Challenge and formulate a concrete roadmap for international cooperation for the next fifteen years.
Workshops
Verified software: from theory to practice
10 May 2021 to 14 May 2021
Verified software: tools and experiments
7 June 2021 to 11 June 2021
Vistas in Verified Software
4 July 2022 to 8 July 2022
Seminars
| Wednesday 13th July 2022 | |||
|---|---|---|---|
| 10:15 to 10:45 |
Angus Hammond University of Cambridge |
Room 2 | 
|
| 10:45 to 11:15 |
Dhruv Makwana University of Cambridge |
Room 2 |
|
| 11:15 to 12:00 |
Lennart Beringer Princeton University |
Room 2 |
|
| 13:30 to 14:00 |
Adam Chlipala Massachusetts Institute of Technology |
Room 2 |
|
| 14:00 to 14:50 |
Ralf Jung Massachusetts Institute of Technology |
Room 2 |
|
| 15:00 to 15:45 |
David Naumann Stevens Institute of Technology |
Room 2 |
|
| Monday 18th July 2022 | |||
|---|---|---|---|
| 10:30 to 12:00 |
Roderick Bloem Graz University of Technology |
Room 2 |
|
| 13:00 to 13:45 |
Supratik Chakraborty Indian Institute of Technology |
Room 2 |
|
| 13:45 to 14:30 |
Synthesis United: Can reactive synthesis and syntax-guided synthesis be friends? - Mark Santolucito |
Room 2 | |
| 14:30 to 15:00 |
Synthesis United: Reactive Synthesis modulo Theories Benedikt Maderbacher |
Room 2 | |
| 15:30 to 16:30 |
Moshe Vardi Rice University |
Discussion Room | |
| 16:30 to 17:00 | Discussion Room | ||
| Wednesday 20th July 2022 | |||
|---|---|---|---|
| 13:30 to 14:00 | Room 2 | ||
| 14:00 to 14:30 | Room 2 | ||
| 14:30 to 15:00 |
Xavier Leroy Collège de France; INRIA |
Room 2 | |
| 15:30 to 16:00 |
Ruzica Piskac Yale University |
Room 2 | |
| 16:00 to 16:30 | Room 2 | ||
| 16:30 to 17:00 |
Benjamin Pierce University of Pennsylvania |
Room 2 | |
| 17:00 to 17:30 |
Michael Greenberg - Teaching Discrete Mathematics to Early Undergraduates using Coq |
Room 2 | |
| Thursday 21st July 2022 | |||
|---|---|---|---|
| 13:30 to 14:30 |
Vytautas Astrauskas |
Room 2 |
|
| 14:30 to 15:30 |
Jacques-Henri Jourdan CNRS (Centre national de la recherche scientifique) |
Room 2 | |
| Friday 22nd July 2022 | |||
|---|---|---|---|
| 09:30 to 10:15 |
Supratik Chakraborty Indian Institute of Technology |
Room 2 | |
| 10:15 to 11:00 |
Elizabeth Polgreen University of Edinburgh |
Room 2 | |
| 11:15 to 12:00 |
Joost-Pieter Katoen RWTH Aachen University; Universiteit Twente |
Room 2 |
|
| 12:00 to 12:45 |
Hana Chockler King's College London |
Room 2 | |
| 14:15 to 15:00 |
Daniel Kroening University of Oxford |
Room 2 | |
| 15:00 to 15:25 |
Kim Larsen Aalborg Universitet |
Room 2 | |
| 16:00 to 16:45 |
Dirk Beyer Ludwig-Maximilians-Universität München |
Room 2 |
|
| 16:45 to 17:30 |
Ziiyad Hanna Cadence design systems; University of Oxford |
Room 2 | |
| Monday 25th July 2022 | |||
|---|---|---|---|
| 11:00 to 12:00 |
Andreas Rossberg None / Other |
Room 2 |
|
| 12:00 to 12:30 | Room 2 | ||
| 14:00 to 15:00 |
Amal Ahmed Northeastern University |
Room 2 | |
| 17:00 to 17:30 | Discussion Room | ||
| Tuesday 26th July 2022 | |||
|---|---|---|---|
| 13:00 to 13:15 | Discussion Room | ||
| 13:15 to 14:00 |
Sanjit Seshia University of California, Berkeley |
Discussion Room | |
| 14:00 to 14:30 |
Hazem Torf |
Discussion Room | |
| 14:30 to 15:00 |
Rupak Majumdar Max Planck Institute for Software Systems |
Discussion Room | |
| 15:30 to 16:00 |
Taylor Johnson |
Discussion Room | |
| 16:00 to 16:30 |
Suman Jana |
Discussion Room | |
| 16:30 to 17:00 |
Wenchao Li |
Discussion Room | |
| 17:00 to 17:30 |
John Rushby |
Discussion Room | |
| Wednesday 27th July 2022 | |||
|---|---|---|---|
| 13:00 to 13:30 |
Naijun Zhan Chinese Academy of Sciences |
Discussion Room | |
| 13:30 to 14:00 |
Andre Platzer Carnegie Mellon University |
Discussion Room | |
| 14:00 to 14:30 |
Sergiy Bogomolov |
Discussion Room | |
| 14:30 to 15:00 |
Yasser Soukry |
Discussion Room | |
| 15:30 to 16:00 |
Chuchu Fan Massachusetts Institute of Technology |
Discussion Room |
|
| 16:00 to 16:30 |
Qi Zhu Northeastern University |
Discussion Room | |
| 16:30 to 17:00 |
Rajeev Alur University of Pennsylvania |
Discussion Room | |
| 17:00 to 17:30 |
Ruzica Piskac Yale University |
Discussion Room |
|
| 17:30 to 18:00 |
Susmit Jha |
Discussion Room | |
| Wednesday 3rd August 2022 | |||
|---|---|---|---|
| 14:00 to 14:15 |
Peter Sewell University of Cambridge |
Room 2 |
|
| 14:15 to 14:30 |
Andrew Appel Princeton University |
Room 2 |
|
| 14:40 to 14:55 |
Bart Jacobs KU Leuven |
Room 2 |
|
| 15:05 to 15:20 |
Michael Sammler Max Planck Institute for Software Systems |
Room 2 |
|
| 15:30 to 15:45 |
Gregory Malecha Bed Rock Systems |
Room 2 |
|
| 15:55 to 16:10 |
Thomas Sewell University of Cambridge |
Room 2 |
|
| 16:20 to 16:35 |
Zhong Shao Yale University |
Room 2 |
|
| 16:40 to 17:00 | Room 2 | ||
| Thursday 11th August 2022 | |||
|---|---|---|---|
| 13:00 to 13:25 |
Matthew Parkinson Microsoft (UK) |
Room 1 |
|
| 13:25 to 13:50 |
Nobuko Yoshida Imperial College London |
Room 1 |
|
| 14:10 to 14:35 |
Fangyi Zhou Imperial College London |
Room 1 |
|
| 14:35 to 15:00 |
Mark Batty |
Room 1 |
|
| 15:00 to 15:25 |
Ben Simner |
Room 1 |
|
| 15:45 to 16:10 |
Viktor Vafeiadis Max Planck Institute for Software Systems |
Room 1 |
|
| 16:10 to 16:45 |
Brijesh Dongol |
Room 1 |
|
| Friday 12th August 2022 | |||
|---|---|---|---|
| 09:00 to 09:25 |
Glynn Winskel University of Cambridge |
Room 1 |
|
| 09:25 to 09:50 |
Esti Fraca University College London |
Room 1 |
|
| 10:10 to 10:35 |
Matthew Windsor University of York |
Room 1 |
|
| 10:35 to 11:00 |
Dan Iorga Imperial College London |
Room 1 |
|
| 11:20 to 11:45 |
Yann Herklotz Imperial College London |
Room 1 |
|
| 11:45 to 12:10 |
Cliff Jones Newcastle University |
Room 1 |
|
Organisers
- Leonardo de Moura Microsoft (UK)
- Azadeh Farzan University of Toronto
- Philippa Gardner Imperial College London
- Kim Larsen Aalborg Universitet
- Xavier Leroy Collège de France; INRIA
- Ken McMillan Microsoft (USA)
- Peter O'Hearn University College London
- Peter Sewell University of Cambridge
- Natarajan Shankar
- Moshe Vardi Rice University
Speakers
- Mark Batty
- Rajeev Alur University of Pennsylvania
- Sanjit Seshia University of California, Berkeley
- Rupak Majumdar Max Planck Institute for Software Systems
- Andrew Appel Princeton University
- Bart Jacobs KU Leuven
- Zhong Shao Yale University
- Gregory Malecha Bed Rock Systems
- Nobuko Yoshida Imperial College London
- Viktor Vafeiadis Max Planck Institute for Software Systems
- Brijesh Dongol
- Glynn Winskel University of Cambridge
- Cliff Jones Newcastle University
- Dirk Beyer Ludwig-Maximilians-Universität München
- Roderick Bloem Graz University of Technology
- Adam Chlipala Massachusetts Institute of Technology
- Amal Ahmed Northeastern University
- Lennart Beringer Princeton University
- Supratik Chakraborty Indian Institute of Technology
- Hana Chockler King's College London
- Joost-Pieter Katoen RWTH Aachen University; Universiteit Twente
- Kim Larsen Aalborg Universitet
- Moshe Vardi Rice University
- Naijun Zhan Chinese Academy of Sciences
- Xavier Leroy Collège de France; INRIA
- David Naumann Stevens Institute of Technology
- Benjamin Pierce University of Pennsylvania
- Ruzica Piskac Yale University
- Peter Sewell University of Cambridge
- Daniel Kroening University of Oxford
- Andre Platzer Carnegie Mellon University
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
- Amal Ahmed Northeastern University
- Aws Albarghouthi University of Wisconsin-Madison
- Andrew Appel Princeton University
- Anindya Banerjee National Science Foundation
- Gilles Barthe Max Planck Institute for Security and Privacy; Max-Planck-Institut für Informatik, Saarbrücken
- Joshua Berdine Facebook Research
- Lennart Beringer Princeton University
- Dirk Beyer Ludwig-Maximilians-Universität München
- Lars Birkedal Aarhus Universitet
- Ahmed Bouajjani Université Paris 7 - Denis-Diderot
- Supratik Chakraborty Indian Institute of Technology
- Javier Esparza Technische Universität München
- Azadeh Farzan University of Toronto
- Philippa Gardner Imperial College London
- Patrice Godefroid Emeritus Researcher of Microsoft Research; Microsoft (USA)
- Timothy Griffin University of Cambridge; Cambridge Computer Laboratory
- Thomas Henzinger IST Austria
- Warren Hunt University of Texas at Austin
- Cliff Jones Newcastle University
- Joost-Pieter Katoen RWTH Aachen University; Universiteit Twente
- Viktor Kuncak EPFL - Ecole Polytechnique Fédérale de Lausanne
- Kim Larsen Aalborg Universitet
- Francesco Logozzo Facebook Research
- Rupak Majumdar Max Planck Institute for Software Systems
- Bernhard Möller Universität Augsburg
- Peter Müller ETH Zürich
- Aditya Nori Microsoft Research - Cambridge
- Lawrence Paulson University of Cambridge
- Benjamin Pierce University of Pennsylvania
- Ruzica Piskac Yale University
- Andrew Pitts University of Cambridge
- Sanjiva Prasad Indian Institute of Technology
- Sanjit Seshia University of California, Berkeley
- Peter Sewell University of Cambridge
- Natarajan Shankar SRI International
- Caterina Urban INRIA
- Moshe Vardi Rice University
- Philip Wadler University of Edinburgh
- Conrad Watt University of Cambridge
- John Wickerson Imperial College London
- Glynn Winskel University of Cambridge
- James Woodcock University of York; Aarhus Universitet
- Naijun Zhan Chinese Academy of Sciences
Supported By
