Machine-Checked Correctness and Complexity of a Union-Find Implementation

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


Duration: 53:40
21 views
0

Union-Find is a famous example of a simple data structure whose amortized asymptotic time complexity analysis is non-trivial. Using Coq and the CFML tool, Arthur Charguéraud and I have verified the correctness and amortized complexity of an OCaml implementation of Union-Find. In this talk, I will give an overview of our approach, which uses higher-order separation logic extended with time credits. This approach allows us to state (and establish) a single specification that covers correctness and complexity at the same time.



Other Videos By Microsoft Research


2016-06-22Nature in the City: Changes in Bangalore over Time and Space
2016-06-22National Parks Conservation Association (NPCA)
2016-06-22Future Microprocessors Driven by Dataflow Principles
2016-06-223D Gesture Recognition through RF Sensing
2016-06-22Unsupervised Latent Faults Detection in Data Centers
2016-06-22Connecting Environmental and Computer Science
2016-06-22Why Visualization? Task Abstraction for Analysis and Design
2016-06-22Inter-Active Learning with Queries on Instances and Features
2016-06-22Speaker Diarization: Optimal Clustering and Learning Speaker Embeddings
2016-06-22Hackathon: Eye Gaze Wheelchair
2016-06-22Machine-Checked Correctness and Complexity of a Union-Find Implementation
2016-06-22Query formulation with Query Auto Completion
2016-06-22Modern Deep Learning through Bayesian Eyes
2016-06-22Crowdsourcing Audio Production Interfaces
2016-06-22Symposium: Algorithms Among Us - Ian Kerr
2016-06-22Opportunities and Challenges in Global Network Cameras
2016-06-22Symposium: Algorithms Among Us - Erik Brynjolfsson
2016-06-22System and Toolchain Support for Reliable Intermittent Computing
2016-06-22Threshold phenomena and social choice
2016-06-22Rethinking Storage and Networking in Next Generation Racks
2016-06-22Provable Algorithms for Learning Neural Networks


Tags:
microsoft research
data sciences
search and information retrieval