Steel: A Concurrent Separation Logic Framework to Scale Up Verification in F*

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


Category:
Vlog
Duration: 53:34
537 views
15

In recent years, the F* ecosystem has been successfully used to formally verify real-world applications ranging from parsers to cryptographic providers. Nevertheless, verification is still time-consuming, and scaling up is still challenging due to (1) lack of modularity when reasoning about the heap, (2) explosion of state-related SMT context and (3) model limited to sequential programming.



In this talk, we present Steel, a concurrent separation logic abstraction on top of the existing F* framework. Steel offers a modular resource-based memory model with permissions, using a mix of SMT solving and F* tactics to discharge its proof obligations. Steel also enables the specification and verification of concurrent programs in a fork-join concurrency model.

See more at https://www.microsoft.com/en-us/research/video/steel-a-concurrent-separation-logic-framework-to-scale-up-verification-in-f/



Other Videos By Microsoft Research


2019-09-04Antennas for light and their applications in classical optics, Dr Rupert Oulton, Imperial College
2019-09-04Photonics for Computing: from Optical Interconnects to Neuromorphic Architectures
2019-09-04Inclusive design for all, or ICT4D and 4U! with Dr. Ed Cutrell [Podcast]
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 2 | Session 4
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 2 | Session 3
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 2 | Session 2
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 1 | Session 4
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 1 | Session 3
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 1 | Session 1
2019-09-03AI Institute "Geometry of Deep Learning" 2019 [Workshop] Day 1 | Session 2
2019-09-03Steel: A Concurrent Separation Logic Framework to Scale Up Verification in F*
2019-09-03Design and Optimization of Dielectric Metasurfaces
2019-08-28HE compilers for Private AI and other game changers with Dr. Olli Saarikivi
2019-08-23Quantum Computing and Workforce, Curriculum, and Application Development: Open Resources
2019-08-23Empowering People to Achieve More: How Useful a Concept is Productivity?
2019-08-23Cars, Computing and the Future of Work: Specific topics of mutual interest
2019-08-23Cars, Computing and the Future of Work: A UW & MSR Workshop: Welcome and Overview
2019-08-22Crowd, Cloud and the Future of Work: Updates from human AI computation
2019-08-22Recommendation and Learning to Improve Personal Productivity
2019-08-22Crowd, Cloud and the Future of Work: Welcome and Updates
2019-08-22Machine reading comprehension with Dr. T.J Hazen


Tags:
microsoft research
programming languages
software engineering
F*