Marrying rely/guarantee and separation logic

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


Category:
Vlog
Duration: 57:19
240 views
0

In the quest for tractable reasoning methods about concurrent algorithms both rely/guarantee logic and separation logic have made great advances, but neither is the ultimate approach. Rely-guarantee copes naturally with interference, but its specifications are complex as they describe the entire state. Conversely, separation logic has difficulty dealing with interference, but its specifications are simpler because they describe only the relevant state that the program accesses. Taking a lock-coupling linked list as an example, I will present a new program logic, RGSep that combines the benefits of the two approaches. RGSep describes interference naturally (using a relation as in rely/guarantee), and where there is no interference, enables local reasoning (as in separation logic). Time permitting; I will demonstrate a prototype tool that automates this reasoning.



Other Videos By Microsoft Research


2016-09-07Graphical Models and Statistical Mechanics in Communications and Storage Applications
2016-09-07Model Abstraction Methodology for Temporal Behavior Analysis of Multiscale Biological Systems
2016-09-07Active Learning with Model Selection in Linear Regression
2016-09-07Human-Centered Home Network Research at Georgia Tech
2016-09-07Imitating the immune system
2016-09-07The Human Experiment: Two Years and Twenty Minutes Inside Biosphere 2           
2016-09-07Structural Abstraction of Software Verification Conditions
2016-09-07Behavior-Based Malware Detection [1/19]
2016-09-07What the Web Means for Science
2016-09-07Textual entailment as a framework for applied semantics
2016-09-07Marrying rely/guarantee and separation logic
2016-09-07Effective Static Race Detection for Java
2016-09-07Temporal Memory Streaming
2016-09-07Multiprocessor Architectures for Programmability
2016-09-07MLP Talk: Modeling Deformable Surfaces from Single Videos
2016-09-07Latent Variables: Bayesian Mixed Graph Models in Supervised and Unsupervised Learning
2016-09-07MSR Technical Education Series: Designing .NET Class Libraries
2016-09-07Ubiquitous Context-Aware Computing: Experience and Emerging Challenges [1/6]
2016-09-07Scalable database replication
2016-09-07Employing decision procedures for automatic program analysis and verification of heap-manipulating
2016-09-07Synthesis from Temporal Specifications


Tags:
microsoft research