Programming with Proofs for High-assurance Software

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=pGIlWfnuTKA


Duration: 16:54
1,805 views
71

Programming critical systems with proofs, a long-standing goal of computer science, is beginning to come within reach of modern programming languages and proof assistants. I provide a brief overview of recent accomplishments in this space, related to work in the F* proof assistant and Project Everest, one of its flagship applications. Programs developed in F* with proofs of correctness are now deployed in wide variety of settings, ranging from Microsoft Windows and Hyper-V, Microsoft Azure, the Linux kernel, Firefox, mbedTLS, and several others production systems.

F* functional programming language: https://fstar-lang.org
Project Everest: https://www.microsoft.com/en-us/research/project/project-everest-verified-secure-implementations-https-ecosystem/



Other Videos By Microsoft Research


2020-09-03Creating Fragments in Microsoft Expressive Pixels (6 of 9)
2020-09-03Managing Animation Galleries in Microsoft Expressive Pixels (5 of 9)
2020-09-03Creating Animations in Microsoft Expressive Pixels (4 of 9)
2020-09-03Creating an Image in Microsoft Expressive Pixels (3 of 9)
2020-09-03Getting Started with Microsoft Expressive Pixels (2 of 9)
2020-09-03Welcome to Microsoft Expressive Pixels (1 of 9)
2020-09-03Importing Animations in Microsoft Expressive Pixels (9 of 9)
2020-09-03Galactic Bell Star Music Demo
2020-09-03Directional Sources & Listeners in Interactive Sound Propagation using Reciprocal Wave Field Coding
2020-09-01Platform for Situated Intelligence Overview
2020-08-28Programming with Proofs for High-assurance Software
2020-08-14From SqueezeNet to SqueezeBERT: Developing Efficient Deep Neural Networks
2020-08-12SkinnerDB: Regret Bounded Query Evaluation using RL
2020-08-07From Paper to Product
2020-08-06Can we make better software by using ML and AI techniques? With Chandra Maddila and Chetan Bansal
2020-08-05MineRL Competition 2020
2020-08-04Directions in ML: Algorithmic foundations of neural architecture search
2020-08-03Microsoft Urban Futures Summer Workshop | Policy and Social Impact [Day 3]
2020-08-03Microsoft Urban Futures Summer Workshop | Sensors and Data [Day 2]
2020-08-03Microsoft Urban Futures Summer Workshop | Data Driven Urban Transformation [Day 1]
2020-07-31Managing Tasks Across the Work-Life Boundary: Opportunities, Challenges, and Directions


Tags:
F*
programming language
High-assurance Software
critical systems
modern programming languages
proof assistants
F* proof assistant
Project Everest
F* functional programming language
microsoft research