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

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


Duration: 53:40
314 views
2

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-13Provable Algorithms for Learning Neural Networks
2016-06-13Modern Deep Learning through Bayesian Eyes
2016-06-13Towards Understandable Neural Networks for High Level AI Tasks; Part 2
2016-06-13Towards Understandable Neural Networks for High Level AI Tasks - Part 4
2016-06-13What are the prospects for automatic theorem proving?
2016-06-13Towards Understandable Neural Networks for High Level AI Tasks - Part 3
2016-06-13Artist in Residence (formerly Studio99) Presents: Michael Gough and "Drawing as Literacy."
2016-06-13Towards Cross-fertilization Between Propositional Satisfiability and Data Mining
2016-06-13Making Objects Count: A Shape Analysis Framework for Proving Polynomial Time Termination
2016-06-13Human factors of software updates
2016-06-13Machine-Checked Correctness and Complexity of a Union-Find Implementation
2016-06-13Applications of 3-Dimensional Spherical Transforms to Acoustics and Personalization of Head-related
2016-06-13Network Protocols: Myths, Missteps, and Mysteries
2016-06-13Optimal and Adaptive Online Learning
2016-06-13Speaker Diarization: Optimal Clustering and Learning Speaker Embeddings
2016-06-13Multi-rate neural networks for efficient acoustic modeling
2016-06-13Unsupervised Latent Faults Detection in Data Centers
2016-06-13System and Toolchain Support for Reliable Intermittent Computing
2016-06-13Gates Foundation Presents: Crucial Areas of Fintech Innovation for the Bottom of the Pyramid
2016-06-13Social Computing Symposium 2016: Harassment, Threats, Trolling Online, Diversity in Gaming is Vital
2016-06-13Bringing Harmony Through AI and Economics


Tags:
microsoft research
union-find