Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

Published in:
Cover of the book

Open Access 2021 | OriginalPaper | Chapter

Bridging Arrays and ADTs in Recursive Proofs

Authors: Grigory Fedyukovich, Gidon Ernst

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer International Publishing

We present an approach to synthesize relational invariants to prove equivalences between object-oriented programs. The approach bridges the gap between recursive data types and arrays that serve to represent internal states. Our relational invariants are recursively-defined, and thus are valid for data structures of unbounded size. Based on introducing recursion into the proofs by observing and lifting the constraints from joint methods of the two objects, our approach is fully automatic and can be seen as an algorithm for solving Constrained Horn Clauses (CHC) of a specific sort. It has been implemented on top of the SMT-based CHC solver AdtChc and evaluated on a range of benchmarks.

download
DOWNLOAD
share
SHARE
print
PRINT
Metadata
Title
Bridging Arrays and ADTs in Recursive Proofs
Authors
Grigory Fedyukovich
Gidon Ernst
Copyright Year
2021
DOI
https://doi.org/10.1007/978-3-030-72013-1_2