Proof Procedures for Separated Heap Abstractions

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


Duration: 47:39
67 views
0

Separation logic is a program logic geared towards reasoning about programs that mutate heap-allocated data structures. This talk describes ideas arising from joint work with Josh Berdine and Cristiano Calcagno on proof procedure for a sublogic of separation logic that is oriented to lightweight program verification and analysis. The proof theory uses ideas from substructural logic together with induction-free reasoning about inductive definitions of heap structures. Substructural reasoning is used to to infer frame axioms, which describe the portion of a heap that is not altered by a procedure, as well as to discharge verification conditions; more precisely, the leaves of failed proofs can give us candidate frame axioms. Full automation is achieved through the use of special axioms that capture properties that would normally be proven using by induction. I will illustrate the proof method through its use in the Smallfoot static assertion checker, where it is used to prove verification conditions and infer frame axioms, as well as in the Space Invader program analysis, where it is used to accelerate the convergence of fixed-point calculations.



Other Videos By Microsoft Research


2016-09-07Microphone Array for Audience Capture in Lecture Rooms
2016-09-07Learning to Label Images
2016-09-07On the Compressibility of NP Instances and Cryptographic Applications
2016-09-07Search: Use of Relevance Feedback and Estimating Effectiveness of Searches
2016-09-07Tool Support for Proof Engineering
2016-09-07Attack-Resistant Algorithms for Massive Networks
2016-09-07Lambda Legal: Making the Case for Equality
2016-09-07Introducing Nielsen Buzzmetrics Research The Global Measurement Standard in Consumer Generated Media
2016-09-07Understanding visual scenes in 200 msec: Results from Human and Modeling Experiments 
2016-09-07Exploiting Multiple Cores Today: Scalability and Reliability For Off-the-shelf Software
2016-09-07Proof Procedures for Separated Heap Abstractions
2016-09-07Client-Side Echo Cancellation for Multi-Party Audio Conferencing
2016-09-07Variance analyses from invariance analyses
2016-09-07Modelling the performance of wireless networks employing the IEEE 802.11 MAC
2016-09-07Geometric Optics, Duality and Congestion in Sensornets [1/2]
2016-09-07All Rise: Somebodies, Nobodies and the Politics of Dignity
2016-09-07Hierarchical Bayesian Models for Rating Individual Players from Group Competitions
2016-09-07Interoperability and natural language processing for business rules engines
2016-09-07Random Matrices and Spectral Clustering Abstract
2016-09-07Generalized Algebraic Data Types and Object-Oriented Programming
2016-09-07Memex Summit (Digital Memories Workshop) - Content-Based Similarity Search with MyLifeBits


Tags:
microsoft research