Skip to main content
Published in:

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

loading …

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.

Bridging Arrays and ADTs in Recursive Proofs
Grigory Fedyukovich
Gidon Ernst
Copyright Year

Premium Partner