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.
> Click here to see the content produced by Plus Magazine during the VSO2 programme
10 May 2021 to 14 May 2021
7 June 2021 to 11 June 2021
4 July 2022 to 8 July 2022
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 | |
Subscribe for the latest updates on events and news
Isaac Newton Institute for Mathematical Sciences, 20 Clarkson Road, Cambridge CB3 0EH United Kingdom
Tel: +44 1223 335999 Email: reception@newton.ac.uk
© 2023 Isaac Newton Institute for Mathematical Sciences. All Rights Reserved. Privacy Policy
INI is a creative collaborative space which is occupied by up to fifty-five mathematical scientists at any one time (and many more when there is a workshop). Some of them may not have met before and others may not realise the relevance of other research to their own work.
INI is especially important as a forum where early-career researchers meet senior colleagues and form networks that last a lifetime.
Here you can learn about all activities past, present and future, watch live seminars and submit your own proposals for research programmes.
Within this section of the website you should find all the information required to arrange and plan your visit to the Institute. If you have any further questions, or are unable to find the information you require, please get in touch with the relevant staff member or our Reception team via our contact pages.
INI and its programme participants produce a range of publications to communicate information about activities and events, publish research outcomes, and document case studies which are written for a non-technical audience. You will find access to them all in this section.
The Isaac Newton Institute aims to maximise the benefit of its scientific programmes to the UK mathematical science community in a variety of ways.
Whether spreading research opportunities through its network of correspondents, offering summer schools to early career researchers, or hosting public-facing lectures through events such as the Cambridge Festival, there is always a great deal of activity to catch up on.
Find out about all of these endeavours in this section of the site.
There are various ways to keep up-to-date with current events and happenings at the Isaac Newton Institute. As detailed via the menu links within this section, our output covers social media streams, news articles, a regular podcast series, an online newsletter, and more detailed documents produced throughout the year.
“A world famous place for research in the mathematical sciences with a reputation for efficient management and a warm welcome for visitors”
The Isaac Newton Institute is a national and international visitor research institute. It runs research programmes on selected themes in mathematics and the mathematical sciences with applications over a wide range of science and technology. It attracts leading mathematical scientists from the UK and overseas to interact in research over an extended period.
INI has a vital national role, building on many strengths that already exist in UK universities, aiming to generate a new vitality through stimulating and nurturing research throughout the country.During each scientific programme new collaborations are made and ideas and expertise are exchanged and catalysed through lectures, seminars and informal interaction, which the INI building has been designed specifically to encourage.
For INI’s knowledge exchange arm, please see the Newton Gateway to Mathematics.
The Institute depends upon donations, as well as research grants, to support the world class research undertaken by participants in its programmes.
Fundraising activities are supported by a Development Board comprising leading figures in academia, industry and commerce.
Visit this section to learn more about how you could play a part in supporting INI’s groundbreaking research.
In this section you can find contact information, staff lists, maps and details of how to find INI’s main building in Cambridge.
Our administrative staff can help you with any queries regarding a prospective or planned visit. If you would like to discuss a proposed a research programme or other event, our senior management team will be happy to help.