Refinement of Thread-Modular Verification

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


Duration: 44:14
39 views
0

Thread-modular verification à la Flanagan and Qadeer is a promising approach for avoiding the state explosion during the verification of concurrent programs. The method is polynomial in the number of threads. It can be phrased as a program analysis with a fixed `Cartesian abstraction'. We propose a flexible refinement of this abstraction that allows one to adapt the precision while preserving the polynomial complexity. Our experimental results demonstrate the practical potential of the resulting method. This is joint work with Andrey Rybalchenko and Andreas Podelski.



Other Videos By Microsoft Research


2016-09-06Learning using Large Datasets
2016-09-06Locating Family Values: A Field Trial of the Whereabouts Clock
2016-09-06VISP: Visualizing Information Search Processes
2016-09-06Dynamics, Emergence and Simulation
2016-09-06User Intention and Interaction for Improving Search Effectiveness
2016-09-06Science Education in the 21st Century: Using the tools of science to teach science
2016-09-06Generic Programming in the Parallel Boost Graph Library
2016-09-06Candidate talk: On the Evaluation and Extraction of Thread-Level Parallelism in Ordinary Programs
2016-09-06Developing the Best Life and Death Solver in Go
2016-09-06No Ifs, Ands, or Buts: Uncovering the Simplicity of Conditionals
2016-09-06Refinement of Thread-Modular Verification
2016-09-06Dependable Software via Automated Verification
2016-09-06GENI - Global Environment for Network Innovations
2016-09-06Welcome - Overview of the day
2016-09-06Mantis and JouleSort: Power Models and Metrics in Enterprise Computing
2016-09-06Explicit-Symbolic Modeling for Formal Verification
2016-09-06Wired Shut: Copyright and the Shape of Digital Culture
2016-09-06Accelerating Architectural-Level Full-System Multiprocessor Simulations using FPGAs
2016-09-06Recurrence of weak graph limits
2016-09-06Power series, power serious
2016-09-06Acoustic Analysis and Modeling of Pathological Voices


Tags:
microsoft research