Skip to main content
main-content

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

Erschienen in:
Buchtitelbild

Open Access 2021 | OriginalPaper | Buchkapitel

Bridging Arrays and ADTs in Recursive Proofs

verfasst von: Grigory Fedyukovich, Gidon Ernst

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

Verlag: 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
TEILEN
print
DRUCKEN
Metadaten
Titel
Bridging Arrays and ADTs in Recursive Proofs
verfasst von
Grigory Fedyukovich
Gidon Ernst
Copyright-Jahr
2021
DOI
https://doi.org/10.1007/978-3-030-72013-1_2