Big Proof - Challenges in Industry and Research

Wednesday 19th July 2017 The Alan Turing Institute London United Kingdom Background

Formal proof systems have been used as constructive demonstrations of mathematical validity for millennia. The generally agreed criteria for formal proofs are that they should have reproducibility (easily accessible and communicable), objectivity (accurately representative) and have verifiability (It being possible to recognise that something is a proof). They are essential in the context of hardware and software systems where formal verification is needed to prove or disprove the correctness of intended algorithms which underpin a systems specification. Formal proofs are used for the verification of systems such as cryptographic protocols, combinational circuits, digital circuits with internal memory and software expressed as source code.

This workshop, part of the Isaac Newton Institute Research Programme Big Proof, brought together mathematicians, computer scientists and logicians with those from relevant application areas. The research programme seeks to explore foundational, theoretical, and practical challenges in exploiting proof technology to transform mathematical practice across a range of scientific and engineering disciplines. A key expected output was a concrete, long-term research agenda for making computational inference a basic technology for formalising, creating, curating, and disseminating mathematical knowledge in digital form.

Aims and Objectives

The aim of the workshop was to promote discussion around the area of big proof and formal verification, and the challenges from academic and industry perspectives. For example, academic challenges are presented by the problem of scaling mathematical proof on machine, including issues such as search, representation and reasoning in ways that are more natural to working mathematicians than current systems offer. Conversely, industry challenges may be posed around the limits of automation and the efficiency of current logics and algorithms.

The Programme of talks featured both academic and industry speakers and included areas such as:

Verification for mainstream software and security Bringing big verification proof to big finance Big proofs from social networks of mathematics Reasoning with big code Reasoning at scale for cloud computing security A key aspect of the workshop was to encourage links between academics and industry and allowed both parties to further understand the others’ needs. Therefore, as well as highlighting state-of-the-art mathematics for formal proof systems, talks also covered end user challenges and experiences. Discussion and networking sessions allowed for new research directions to be discussed and areas of mutual interest were explored.

Registration and Venue

Registration for this event is now closed.

The workshop took place at the Alan Turing Institute, London. The Institute is headquartered at the British Library. Please see the link for directions to the venue.

Organisers

Professor David Aspinall (University of Edinburgh and Alan Turing Institute) and David Butler (Alan Turing Institute)