|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Graph-Based Reasoning in Separation Logic for Fun and Profit
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.
This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending
In this talk, I will present a graph-based approach to reasoning in a fragment of Separation Logic with pointers and linked lists which gives new complexity bounds and new algorithms for standard reasoning procedures outperforming state-of-the-art reasoners up to several orders of magnitude. Separation Logic is an extension of Hoare logic that enables the efficient verification of programs that manipulate dynamically allocated data structures. Over the last couple of years, fragments of Separation Logic with decidable inference problems have successfully been employed in tools such as Smallfoot, SpaceInvader or SLAyer to automatically verify industrial low-level systems code. The applicability and scalability of these tools heavily depends on the computational costs of the underlying reasoning procedures. In the aforementioned tools, the implemented reasoning procedures for the fragment of Separation Logic with pointers and linked lists proceed via a syntactic proof search, which gives a worst-case exponential running time. I will present a recently introduced approach to entailment checking in this fragment which is based on graph-theoretic methods and allows for polynomial-time reasoning. Alongside with settling an open problem about the complexity of entailment in this fragment and providing highly competitive reasoning procedures, this approach also yields nice algorithms for other reasoning problems such as frame inference. I will conclude my talk discussing limitations and possible directions for future work.
This talk is part of the Microsoft Research Cambridge, public talks series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsEPRG Energy and Environment Seminar Series Lent 2009 Horizon Forum: The Cell-Materials Interface Medicine for the Elderly
Other talks'Mutant stem cell behaviour in squamous carcinogenesis' Ex Oriente Lux: the legacy of Lukács, Mannheim and Hauser Targeting immune checkpoints and the tumour microenvironment to fight cancer 1st year seminars 2015, session 5 On the origin of animals, and the intervention of the modern biosphere The Surrey Communication and Language in Education Study (SCALES): a population study of language impairment at school entry