COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Automating reasoning tasks for separation logic

## Automating reasoning tasks for separation logicAdd to your list(s) Download to your calendar using vCal - Juan A. Navarro PĂ©rez, UCL
- Friday 17 January 2014, 16:00-17:00
- Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.
If you have a question about this talk, please contact Jonathan Hayman. One of the main goals of program analysis and verification is to develop fully automated tools that can reason efficiently about as many programs as possible. However, scalable automated reasoning is still among the main challenges for programs which operate on user-defined data structures on the heap. In this talk I will give an overview of recent work on the automation of separation logic, a formalism which has proved quite powerful for reasoning about such data structures. I will introduce the basic techniques behind a decision procedure for entailment checking on a fragment of the logic restricted to list segments, and describe how such techniques are generalised in two directions: to provide combined reasoning with other theories (SMT), and to decide the satisfiability of inductive definitions of arbitrary heap shapes. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
- Computer Laboratory talks
- Computing and Mathematics
- Logic and Semantics Seminar (Computer Laboratory)
- School of Technology
Note that ex-directory lists are not shown. |
## Other listsAlgebra Seminar Cardiovascular Epidemiology Unit Special Seminars Cambridge Drosophila Seminar Series## Other talksTitle: TBA (Prof. Robert L. Stamps, University of Glasgow) TBC Recent Theoretical Advances in the Control of Quantum Continuous Variables The 2014 Innate Immunity Summit CGHR Research Group Under pressure: Environmental stressors alter relationships between physiology and behaviour in fishes |