Decision procedures for algebraic data types with abstractions

DOI10.1145/1706299.1706325zbMath1312.68147OpenAlexW2162315884MaRDI QIDQ5255074

Viktor Kuncak, Philippe Suter, Mirco Dotta

Publication date: 11 June 2015

Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1706299.1706325

zbMATH Keywords

decision proceduredata structurealgebraic data typecatamorphism

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Data structures (68P05)

Related Items (14)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ A First-Order Logic with Frames ⋮ Modular Termination and Combinability for Superposition Modulo Counter Arithmetic ⋮ A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited ⋮ Reasoning about algebraic data types with abstractions ⋮ Solving constrained Horn clauses over algebraic data types ⋮ A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ Unnamed Item ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Towards Complete Reasoning about Axiomatic Specifications ⋮ Decision Procedures for Automating Termination Proofs ⋮ Sets with Cardinality Constraints in Satisfiability Modulo Theories ⋮ Politeness and combination methods for theories with bridging functions ⋮ Reasoning in the theory of heap: satisfiability and interpolation

This page was built for publication: Decision procedures for algebraic data types with abstractions