Transition Invariants

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


Duration: 44:31
659 views
2

Proof rules for the temporal verification of concurrent programs rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invariants. A transition invariant of a program is a binary relation over program states that contains the transitive closure of the transition relation of the program. A transition invariant is disjunctively well-founded if it is a finite union of well-founded relations. We characterize the validity of a liveness property by the existence of a disjunctively well-founded transition invariant.



Other Videos By Microsoft Research


2016-09-05Distributed Multi-robot Exploration and Mapping
2016-09-051.Vision: Extraordinary Computing Experiences & 2. Robots for the Masses: Fiction or Reality
2016-09-05Modeling and Facilitating Human Communication [1/5]
2016-09-05Reducing Errors in Computer Recognition of Handwritten Material
2016-09-05Information wants to be free (but is everywhere in chains)
2016-09-05The art and technology of electronic textiles
2016-09-05Quantum Loop Gas Approach to Topological Phases of Correlated Electrons
2016-09-05Computational History In Action: Discovering Gutenberg's Printing Process
2016-09-05A World Filled With Cameras: Security at the Cost of Freedom? Or Can We Have Both?
2016-09-05Resisting Denial of Service Attacks by Puzzle Outsourcing
2016-09-05Transition Invariants
2016-09-05Declarative querying of sensor networks through automatic service planning
2016-09-05Folklore of Network Protocol Design (Anita Borg Lecture)
2016-09-05Toolkit for Construction and Maintenance of Extensible Proof Search Tactics
2016-09-05ME++
2016-09-05Structural Comparison of Executable Objects
2016-09-05Indifference is Death: Responsibility, Leadership, & Innovation
2016-09-05TQFTs and tight contact structures on 3-manifolds      
2016-09-05Wireless Embedded Networks/The Ecosystem and Cool Challenges
2016-09-05Data Mining & Machine Learning to empower business strategy
2016-09-05Some uses of orthogonal polynomials


Tags:
microsoft research