Decision procedures for algebraic data types with abstractions

DOI10.1145/1706299.1706325zbMath1312.68147MaRDI 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 procedure; data structure; algebraic data type; catamorphism

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q65: Abstract data types; algebraic specification

68P05: Data structures

Related Items

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