skip to content
 

Verified software

Participation in INI programmes is by invitation only. Anyone wishing to apply to participate in the associated workshop(s) should use the relevant workshop application form.

Programme
27th July 2020 to 4th September 2020
Organisers: 
Natarajan Shankar SRI International
Leonardo de Moura Microsoft (USA)
Azadeh Farzan University of Toronto
Philippa Gardner Imperial College London
Tony Hoare Isaac Newton Institute
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
Moshe Vardi Rice University

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.

 

University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons