Milner Lecture: Philippa Gardner Interview with Philippa Gardner As part of the 60 years of computer science and AI celebration, distinguished researchers from both disciplines have been invited to visit the School of Informatics. We have asked them to tell us about their research. Philippa Gardner is a professor in the Department of Computing at Imperial College London. Milner Lectures The Milner Lecture was endowed by the late and much-missed Robin Milner when he left Edinburgh for Cambridge, and is for a public lecture by someone outside Edinburgh who is doing "excellent theoretical work with a perceived application to practice". In this year of celebration, our speakers were asked to set their work in the context of the history of theoretical computer science at Edinburgh. As part of the celebrations of 60 years of Computer Science and Artificial Intelligence at Edinburgh, the Laboratory for Foundations of Computer Science held a special series of three Milner Lectures given by former members of LFCS. Title: Verified Software Specification at Scale Lecture abstract Software should be judged on fundamental engineering principles, with rigorous answers to questions such as: ‘What does this software do and not do?; ‘Does the software behave as intended?’; and ‘How do we trust the answers to such questions?’. Such answers are especially important for the reliability of our modern, complex, continually-evolving software systems which cannot be guaranteed by the established, non-mathematical techniques such as informal prose specification and ad-hoc testing. It has been the dream of many in the computer science community to use machine-supported reasoning to bring scientific, mathematical method to the specification and verification of modern software systems, as originally proposed in Turing’s paper, “Checking a Large Routine” (1949), Hoare’s paper “An Axiomatic Basis for Computer Programming” (1969) and Milner's paper "Logic for Computable Functions (LCF): Description of a Machine Implementation" (1972). Academics and industrial specialists have made great strides in formal software reasoning: proof assistants are mature; verification tools are tractable; and real-world programs are being formally specified and verified in academia and industry. Recently, fundamental mathematical techniques and well-engineered tools have been used to reason about open industrial software at scale. This dream is beginning to become a reality. In this talk, I will provide a whirl-wind tour of recent work by myself and many others on the specification and verification of language standards, libraries and general programs, in each case discussing what it means for the specification to be appropriate, properly evaluated and useful for real-world applications. In particular, I will touch on: the mechanised specification of the W3C WebAssembly language standard, a low-level language supported by all major Web browsers and designed primarily to be an efficient compilation target for C, C++ and Rust. WebAssembly modules, inspired by Milner's ML modules, have provably strong encapsulation properties, and the formal language standard is directly inspired by Milner's formal ML definition based on Plotkin's structured operational semantics. compositional techniques and industrial-strength tools for verification and true bug-finding using ideas from separation logic, a modern Hoare logic inspired by Burstall's early work on proving the correctness of programs which alter data structures. The compositionality of the approach means that functions can be specified locally, independent of the possibly large codebase in which they reside. This locality property is essential for the success of Meta's compositional analysis tool INFER. compositional techniques for the verification of complex shared-memory concurrent programs, with two-sided abstract specifications of concurrent operations: implementations can be proved correct with respect to a function specification; and clients calling a function can be verified using its specification. This fundamental work led to the verification of some of the most advanced examples of concurrent behaviour (e.g. skip-lists in java.util.concurrent), and underpins the Coq-mechanised Iris verification framework which has hundreds of specialist users and has been applied, for example, to find bugs in unsafe Rust code, to verify properties of a Meta hypervisor, and to provide the ‘bedrock’ of the industrial Bedrock hypervisor. Despite these quite considerable advances, we still have much to do to bring scientific, mathematical method to the specification and verification of our modern software systems. Speaker's bio: Philippa Gardner Philippa Gardner is a professor in the Department of Computing at Imperial College London and has a UK Research and Innovation Established Fellowship from 2018–2023. Her research focusses on program specification and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction. Gardner completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship at Imperial, 2005-2009. In 2020 she was elected a Fellow of the Royal Academy of Engineering. Philippa was the director of the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, 2017-2023. Philippa is the general Chair for POPL '24, the 50th Annual ACM SIGPLAN Symposium on Principles of Programming Languages to be held in London, in January 2024 and was also an organiser of the Isaac Newton Institute six-week summer programme on `Verified Software', 2022. May 04 2023 12.00 - 14.00 Milner Lecture: Philippa Gardner Milner Lecture: Verified Software Specification at Scale | Speaker: Philippa Gardner, a professor in the Department of Computing at Imperial College London G.07, Informatics Forum
Milner Lecture: Philippa Gardner Interview with Philippa Gardner As part of the 60 years of computer science and AI celebration, distinguished researchers from both disciplines have been invited to visit the School of Informatics. We have asked them to tell us about their research. Philippa Gardner is a professor in the Department of Computing at Imperial College London. Milner Lectures The Milner Lecture was endowed by the late and much-missed Robin Milner when he left Edinburgh for Cambridge, and is for a public lecture by someone outside Edinburgh who is doing "excellent theoretical work with a perceived application to practice". In this year of celebration, our speakers were asked to set their work in the context of the history of theoretical computer science at Edinburgh. As part of the celebrations of 60 years of Computer Science and Artificial Intelligence at Edinburgh, the Laboratory for Foundations of Computer Science held a special series of three Milner Lectures given by former members of LFCS. Title: Verified Software Specification at Scale Lecture abstract Software should be judged on fundamental engineering principles, with rigorous answers to questions such as: ‘What does this software do and not do?; ‘Does the software behave as intended?’; and ‘How do we trust the answers to such questions?’. Such answers are especially important for the reliability of our modern, complex, continually-evolving software systems which cannot be guaranteed by the established, non-mathematical techniques such as informal prose specification and ad-hoc testing. It has been the dream of many in the computer science community to use machine-supported reasoning to bring scientific, mathematical method to the specification and verification of modern software systems, as originally proposed in Turing’s paper, “Checking a Large Routine” (1949), Hoare’s paper “An Axiomatic Basis for Computer Programming” (1969) and Milner's paper "Logic for Computable Functions (LCF): Description of a Machine Implementation" (1972). Academics and industrial specialists have made great strides in formal software reasoning: proof assistants are mature; verification tools are tractable; and real-world programs are being formally specified and verified in academia and industry. Recently, fundamental mathematical techniques and well-engineered tools have been used to reason about open industrial software at scale. This dream is beginning to become a reality. In this talk, I will provide a whirl-wind tour of recent work by myself and many others on the specification and verification of language standards, libraries and general programs, in each case discussing what it means for the specification to be appropriate, properly evaluated and useful for real-world applications. In particular, I will touch on: the mechanised specification of the W3C WebAssembly language standard, a low-level language supported by all major Web browsers and designed primarily to be an efficient compilation target for C, C++ and Rust. WebAssembly modules, inspired by Milner's ML modules, have provably strong encapsulation properties, and the formal language standard is directly inspired by Milner's formal ML definition based on Plotkin's structured operational semantics. compositional techniques and industrial-strength tools for verification and true bug-finding using ideas from separation logic, a modern Hoare logic inspired by Burstall's early work on proving the correctness of programs which alter data structures. The compositionality of the approach means that functions can be specified locally, independent of the possibly large codebase in which they reside. This locality property is essential for the success of Meta's compositional analysis tool INFER. compositional techniques for the verification of complex shared-memory concurrent programs, with two-sided abstract specifications of concurrent operations: implementations can be proved correct with respect to a function specification; and clients calling a function can be verified using its specification. This fundamental work led to the verification of some of the most advanced examples of concurrent behaviour (e.g. skip-lists in java.util.concurrent), and underpins the Coq-mechanised Iris verification framework which has hundreds of specialist users and has been applied, for example, to find bugs in unsafe Rust code, to verify properties of a Meta hypervisor, and to provide the ‘bedrock’ of the industrial Bedrock hypervisor. Despite these quite considerable advances, we still have much to do to bring scientific, mathematical method to the specification and verification of our modern software systems. Speaker's bio: Philippa Gardner Philippa Gardner is a professor in the Department of Computing at Imperial College London and has a UK Research and Innovation Established Fellowship from 2018–2023. Her research focusses on program specification and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction. Gardner completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship at Imperial, 2005-2009. In 2020 she was elected a Fellow of the Royal Academy of Engineering. Philippa was the director of the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, 2017-2023. Philippa is the general Chair for POPL '24, the 50th Annual ACM SIGPLAN Symposium on Principles of Programming Languages to be held in London, in January 2024 and was also an organiser of the Isaac Newton Institute six-week summer programme on `Verified Software', 2022. May 04 2023 12.00 - 14.00 Milner Lecture: Philippa Gardner Milner Lecture: Verified Software Specification at Scale | Speaker: Philippa Gardner, a professor in the Department of Computing at Imperial College London G.07, Informatics Forum
May 04 2023 12.00 - 14.00 Milner Lecture: Philippa Gardner Milner Lecture: Verified Software Specification at Scale | Speaker: Philippa Gardner, a professor in the Department of Computing at Imperial College London
