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) > Cyclic Abduction of Inductive Termination Preconditions
Cyclic Abduction of Inductive Termination PreconditionsAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Jonathan Hayman. The question “does program P terminate, given precondition X?” is a classic one in program analysis. In this talk, we aim to go a bit further and ask the following abduction question: “can we find a reasonable precondition X under which P terminates?”. When one considers heap-manipulating programs, this problem typically involves inventing the inductive definitions of data structures. For example, a program that traverses “next” fields of pointers until it reaches “nil” will terminate given a heap structured as an acyclic list as input. But given a cyclic list, it will fail to terminate, and given something that is not a list at all, it will typically encounter a memory fault and crash. Here we demonstrate a new heuristic method, called cyclic abduction, for automatically inferring the inductive definitions of termination preconditions for heap-manipulating programs. That is, given a program, this method returns the definition of an inductively defined predicate in separation logic under which the program is guaranteed to terminate (without crashing). Cyclic abduction essentially works by searching for a cyclic proof of termination of the program, abducing definitional clauses of the precondition as necessary to advance the proof search process. We have implemented cyclic abduction in an automated tool, which is capable of finding natural termination preconditions for a range of small programs. The abduced predicates may define segmented, cyclic, nested, and/or mutually defined data structures. This is joint work with Nikos Gorogiannis (also at UCL ). This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCambridge AWiSE Cambridge University Global Health Student Initiative - Seminar Series Fitzwilliam College Linguists' Events Current Issues in Assessment Biophysical Techniques Lecture Series 2015 EnvironmentOther talksLiver Regeneration in the Damaged Liver Psychological predictors of risky online behaviour: The cases of online piracy and privacy A tale of sleepless flies and ninna nanna. How Drosophila changes what we know about sleep. Prescribing step counts in type 2 diabetes and hypertension:Results of the Step Monitoring to improve ARTERial health trial Beacon Salon # 8 The Dawn of the Antibiotic Age The Anne McLaren Lecture: CRISPR-Cas Gene Editing: Biology, Technology and Ethics BP KEYNOTE LECTURE: Importance of C-O Bond Activation for CO2/COUtilization - An Approach to Energy Conversion and Storage Symplectic topology of K3 surfaces via mirror symmetry Coin Betting for Backprop without Learning Rates and More The role of myosin VI in connexin 43 gap junction accretion |