Bi-Abductive Inference for Shape and Ordering Properties

Chris Curry, Quang Loc Le, Shengchao Qin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

68 Downloads (Pure)

Abstract

In separation logic, bi-abduction - a combination
of abductive inference and frame inference - is the key enabler
for compositional reasoning, helping to scale up verification
significantly. Indeed, the success of bi-abduction led to the
development of Infer, the tool used daily to verify Facebook’s codebase of millions of lines of code. However, this success currently stays largely within the shape domain. To extend this impact towards the combination of shape and arithmetic domains, in this work, we present a novel one-stage bi-abductive procedure for a combination of data structures and ordering values. The procedure is designed in the spirit of the Unfold-and-Match paradigm where the inference is utilized to derive any mismatched portion. We demonstrate our proposal through several interesting examples to show that it is promising for an automated verification of heap-manipulating programs.
Original languageEnglish
Title of host publicationthe 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019)
PublisherIEEE
Publication statusPublished - 26 Aug 2019
Event24th International Conference on Engineering of Complex Computer Systems - , Hong Kong
Duration: 10 Nov 201913 Nov 2019
http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=89043&copyownerid=112121

Conference

Conference24th International Conference on Engineering of Complex Computer Systems
Abbreviated titleICECCS 2019
CountryHong Kong
Period10/11/1913/11/19
Internet address

Fingerprint Dive into the research topics of 'Bi-Abductive Inference for Shape and Ordering Properties'. Together they form a unique fingerprint.

  • Cite this

    Curry, C., Le, Q. L., & Qin, S. (2019). Bi-Abductive Inference for Shape and Ordering Properties. In the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019) IEEE. https://ieeexplore.ieee.org/abstract/document/8882771