Practical Boogie (on the example of VCC)

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


Duration: 58:31
487 views
7

IΓÇÖm going to talk about encoding various constructs in Boogie. In particular IΓÇÖll focus on object invariants, as implemented in VCC, and what can be built on them: ownership, counting permissions for concurrent programs, recursive data-structures, and secrecy properties. IΓÇÖll also talk about encoding data-types, termination checking, and induction proofs. VCC is a verifier of complex, user-supplied properties of concurrent C programs. It builds on top of Boogie, an intermediate verification language, generating verification conditions for various provers including Z3.



Other Videos By Microsoft Research


2016-08-16Understanding Visual Scenes: Where are We?
2016-08-16Energy Functionals: Choices and Consequences For Medical Image Segmentation
2016-08-16Abelian Sandpiles and the Harmonic Model
2016-08-16Full-rank Gaussian Modeling of Convolutive Audio Mixtures Applied to Source Separation
2016-08-16MADDER and Self-Tuning Data Analytics on Hadoop with Starfish
2016-08-16Approximation Algorithms for Correlated Knapsacks and Non-Martingale Bandits
2016-08-16ChatArt: Interactive Pictographic Chat
2016-08-16Nonnegative k-sums, fractional covers, and probability of small deviations
2016-08-16Injective Tensor Norms: Hardness and Reductions
2016-08-16Monitoring Untrusted Modern Applications with Collective Record and Replay
2016-08-16Practical Boogie (on the example of VCC)
2016-08-16Coherent Depth in Stereo Vision
2016-08-16Multi-microphone Dereverberation and Intelligibility Estimation in Speech Processing
2016-08-16From Personalized Retinal Image Mapping to Large Scale Parallel Image Processing
2016-08-16Coding4Fun XAPfest!
2016-08-16Your Abstractions are Worth Powerless! Non-Volatile Storage and Computation on Embedded Devices
2016-08-16Near Optimal Online Algorithms and Fast Approximation Algorithms for Resource Allocation Problems
2016-08-16Interpreting the Community: Information Practices and/for Deviance
2016-08-16Pretty Good Democracy for a variety of voting schemes
2016-08-16Learning Valuation Functions
2016-08-16Applying Semantic Analyses to Content-based Recommendation and Document Clustering


Tags:
microsoft research