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.
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 language | English |
|---|---|
| Title of host publication | the 24th International Conference on Engineering of Complex Computer Systems (ICECCS 2019) |
| Publisher | IEEE |
| Publication status | Published - 26 Aug 2019 |
| Event | 24th International Conference on Engineering of Complex Computer Systems - , Hong Kong Duration: 10 Nov 2019 → 13 Nov 2019 http://www.wikicfp.com/cfp/servlet/event.showcfp?eventid=89043©ownerid=112121 |
Conference
| Conference | 24th International Conference on Engineering of Complex Computer Systems |
|---|---|
| Abbreviated title | ICECCS 2019 |
| Country/Territory | Hong Kong |
| Period | 10/11/19 → 13/11/19 |
| Internet address |