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
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
