Decision procedures for algebraic data types with abstractions
From MaRDI portal
Publication:5255074
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
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