Daniel Kröning

Senior Principal Scientist, Amazon

Daniel Kröning is a Senior Principal Scientist at Amazon Web Services (AWS). He was a Professor of Computer Science at the Department of Computer Science at the University of Oxford until 2020, and assistant professor at the Swiss Technical Institute (ETH) in Zürich, Switzerland, from 2004 to 2007. He is co-founder of Diffblue, a university spin-out that automates software engineering tasks.

Xavier Leroy

Professor in Software Sciences at Collège de France and member of the Inria Cambium research team.

Xavier Leroy is professor of software sciences at Collège de France in Paris, and member of the Cambium research team of Inria Paris.  His research interests include programming languages and systems, and the formal verification of software for safety and security.  He is the architect and lead developer of the OCaml programming language and its implementation, one of the most widely-used typed functional programming languages. 

His current work focuses on the formal verification of programming tools, and especially on the CompCert verified C compiler, the first realistic compiler that has been mathematically proved correct. 

He is a Fellow of the ACM and received the 2007 Monpetit award of the French Academy of sciences, the 2016 Milner award of the Royal Society, and the 2018 Grand Prix of Inria and the French Academy of sciences.  He serves as area editor for the Journal of the ACM and has served as co-editor in chief for the Journal of Functional Programming.

Greg Morrisett

Dean and Vice Provost of Cornell Tech, Cornell University.

Greg Morrisett is the Dean and Vice Provost of Cornell Tech, a New York City-based campus focused on graduate education that integrates technology, business, law, and design in service of economic impact and societal good. Previously, Greg served as the Dean of Computing and Information Sciences (CIS) at Cornell University, which houses the departments of Computer Science, Information Science, and Statistical Sciences. Before this, he held the Allen B. Cutting Chair in Computer Science at Harvard University from 2004-2015. 

Professor Morrisett's research focuses on the application of programming language technology for building secure, reliable, and high-performance software systems. A common theme is the focus on systems-level languages and tools that can help detect or prevent common vulnerabilities in software. Past examples include typed assembly language, proof-carrying code, software fault isolation, and control-flow isolation. Recently, his research focuses on building provably correct and secure software, including a focus on cryptographic schemes, machine learning, and compilers.

Morrisett is a Fellow of the ACM and has received a number of awards for his research on programming languages, type systems, and software security, including a Presidential Early Career Award for Scientists and Engineers, an IBM Faculty Fellowship, an NSF Career Award, and an Alfred P. Sloan Fellowship. He served as editor on a number of journals and on the DARPA Information Science and Technology Study (ISAT) Group, the NSF Computer and Information Science and Engineering (CISE) Advisory Council, The Max Planck Institute for Software Systems Advisory Board, the Computing Research Association Board, Microsoft Research's Technical Advisory Board, Microsoft's Trusthworthy Computing Academic Advisory Board, and the Fortify Technical Advisory Board.

Peter O’Hearn

Distinguished Engineer at Lacework and Professor at UCL

Peter O'Hearn is a Distinguished Engineer at Lacework and a Professor at University College London. Peter has done research in the broad areas of programming languages and logic, and held academic positions at Syracuse University, Queen Mary University of London, and University College London, and he worked at Meta from 2013-2021; he joined Meta with the acquisition of the verification startup Monoidics.

With John Reynolds Peter devised Separation Logic, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter's team at Meta. Infer runs internally on Facebook's code bases, and has detected hundreds of thousands of bugs which have been fixed by Facebook's developers before reaching products. Infer is also used in production at number of other companies, including Amazon, Microsoft and Mozilla, and is deployed to many other organizations through the Sonatype Lift analysis platform.

Most recently Peter developed Incorrectness Logic, a theory aimed at providing a foundation for bug catching tools based on proofs of the presence of bugs. Peter is a  Fellow of the Royal Society (elected 2018), a Fellow  of the Royal Academy of Engineering (2016), he has received a number of  awards for his work including the 2016 Gödel Prize, the 2016 CAV Award, the 2021 IEEE Cybersecurity Award for Practice, and he received an honorary doctorate from Dalhousie University in 2018.

Martin Sadler

Special Advisor to the VC on Industrial Strategy, University of Bristol

Martin Sadler was previously Vice President of Hewlett Packard Labs in Bristol, directing the company’s exploratory and advanced research in security and large-scale system management.

He was also member of the advisory board for the Government’s Foresight Cyber Trust and Crime Prevention project and of the board for The Institute of Information Security Professional. He served as a member of the steering committee for the Government’s Cyber Security Knowledge Transfer Network and as a member of the Confederation of British Industry's Information Security working group. Martin was awarded his OBE in 2013 for services to science.

Peter Sewell

Professor of Computer Science, University of Cambridge

Peter Sewell is a Professor of Computer Science at the University of Cambridge.  His research aims to build rigorous foundations for the engineering of real-world computer systems, to make them better-understood, more robust, and more secure.

He and his colleagues have helped clarify the concurrent and sequential behaviour of the architectures and languages underlying much of our computational infrastructure (Arm-A, RISC-V, x86, IBM Power, and C/C++), showing how one can precisely define, validate, and reason about mathematically precise characterisations of these full-scale industrial interfaces, to enhance traditional non-formal engineering.  

Within the CHERI project, developing architecture and language support for hardware capabilities to improve mainstream system security, this work has shown how one can prove that the full-scale Arm Morello architecture guarantees its intended security properties. 

Jules Villard

Software Engineer in the Static Analysis Tools team at Meta.

Jules Villard is a Software Engineer in the Static Analysis Tools team at Meta, leading the development of the Infer open-source static analysis platform. Each month at Meta, Infer prevents hundreds of issues from reaching production by analysing hundreds of code changes daily inside tens of millions of lines of code written in Java, C, C++, Objective-C, and more. Infer is used by several other companies and projects, some of which actively contribute to its development.

Jules' research interests lie in programming languages and mathematical logic, especially when applied to finding bugs in programs at scale or to reasoning about programs in a compositional way. In particular, Jules has contributed new compositional program logic techniques for proving correct programs that manipulate data structures with arbitrary sharing, and programs communicating via message passing over a shared memory.

Jules created the Pulse memory and value analyses engine inside Infer, which underpins several Infer analyses and bug types and has inspired foundational work in under-approximate reasoning for proving the presence of bugs.

Prior to joining Meta in 2015, Jules obtained a PhD from ENS Cachan in 2011 and held post-doc positions across London at Queen Mary University London, University College London, and Imperial College London.