Cyclic abduction of inductively defined safety and termination preconditions

Conference paper


Brotherston, J. and Gorogiannis, N. 2014. Cyclic abduction of inductively defined safety and termination preconditions. 21st International Static Analysis Symposium, SAS 2014. Munich, Germany 11 - 13 Sep 2014 Springer. https://doi.org/10.1007/978-3-319-10936-7_5
TypeConference paper
TitleCyclic abduction of inductively defined safety and termination preconditions
AuthorsBrotherston, J. and Gorogiannis, N.
Abstract

We introduce cyclic abduction: a new method for automatically inferring safety and termination preconditions of heap manipulating while programs, expressed as inductive definitions in separation logic. Cyclic abduction essentially works by searching for a cyclic proof of the desired property, abducing definitional clauses of the precondition as necessary in order to advance the proof search process.
We provide an implementation, Caber, of our cyclic abduction method, based on a suite of heuristically guided tactics. It is often able to automatically infer preconditions describing lists, trees, cyclic and composite structures which, in other tools, previously had to be supplied by hand.

Research GroupFoundations of Computing group
Conference21st International Static Analysis Symposium, SAS 2014
ISSN0302-9743
ISBN
Hardcover9783319109350
PublisherSpringer
Publication dates
Print2014
Publication process dates
Deposited12 May 2015
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-10936-7_5

Additional information

Published paper appears in: Static Analysis, Volume 8723 of the series Lecture Notes in Computer Science, pp 68-84

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-10936-7_5
LanguageEnglish
Book titleStatic Analysis: 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings
Permalink -

https://repository.mdx.ac.uk/item/854xw

Download files


Accepted author manuscript
  • 14
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as