Automated Assume-guarantee Verification

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


Duration: 1:11:13
538 views
3

Assume-guarantee reasoning is a ΓÇ£divide and conquerΓÇ¥ approach to the verification of large systems that makes use of assumptions about the environment of a system component. Coming up with appropriate assumptions used to be a difficult manual process. We will present recently developed techniques for performing assume-guarantee verification of software in a fully automated fashion. These techniques generate assumptions that model the operational context of a component when checking the component in isolation. We will describe learning-based and abstraction-based techniques that build and update assumptions in a systematic and iterative fashion. We will also discuss the application of the techniques to a number of NASA case studies. (joint work with D. Giannakopoulou and other people)



Other Videos By Microsoft Research


2016-09-06Network Data Streaming - A Computer Scientist's Journey in Signal Processing
2016-09-06Exa-Scale Volunteer Computing
2016-09-06On Evaluating Language Technologies
2016-09-06Designing a Virtual Information Telescope Using Mobile Phones and Social Participation [1/2]
2016-09-06Edge-Preserving Decomposition for Multi-Scale Tone and Detail Manipulation
2016-09-06Brain in a Bottle, Structure and Algorithms
2016-09-06Building Mashups by Example
2016-09-06Analyzing Metabolomics Data for Automated Prediction of Underlying Biological Mechanisms
2016-09-06Examining Bugs to Improve Static Analysis
2016-09-06Towards Programmable Matter
2016-09-06Automated Assume-guarantee Verification
2016-09-06EUCALYPTUS: An Open Source Service Infrastructure for Elastic Computing Research
2016-09-06Donnybrook: Enabling Large-Scale, High-Speed, Peer-to-Peer Games
2016-09-06Model Compression
2016-09-06Tidbits Gleaned Over Nine Years of Concurrent Software Testing Research
2016-09-06Pig: Dataflow Programming for Map-Reduce Clusters
2016-09-06Symbolic (Java) PathFinder - Symbolic Execution of Java bytecodes
2016-09-06Understanding the Productivity Gridlock in Scientific Computing (and can Software Engineering Help)
2016-09-06Compressive Sensing
2016-09-06Releasing Human Adaptive Power through Design Innovation [1/3]
2016-09-06Enhancing the Musical Experience - From the Acoustic to the Digital... and Back.


Tags:
microsoft research