Brotherston, J; Gorogiannis, N; (2014) Cyclic abduction of inductively defined safety and termination preconditions. In: Cyclic Abduction of Inductively Defined Safety and Termination Precondition. (pp. 68 - 84). Springer International Publishing: Switzerland.

Preview

PDF cyclic_abduction_SAS14.pdf Available under License : See the attached licence file. Download (434kB)

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.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as XMLJSONCSV

Archive Staff Only

View Item