Reasoning about algebraic data types with abstractions

DOI10.1007/s10817-016-9368-2zbMath1386.68104arXiv1603.08769OpenAlexW2331781799MaRDI QIDQ1694026

Tuan-Hung Pham, Andrew Gacek, Michael W. Whalen

Publication date: 1 February 2018

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1603.08769

zbMATH Keywords

SMT solversdecision proceduresalgebraic data types

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Related Items

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses, Solving constrained Horn clauses over algebraic data types, Unnamed Item, Politeness and combination methods for theories with bridging functions, Removing algebraic data types from constrained Horn clauses using difference predicates

Uses Software

• ACL2
• Dafny
• Isabelle/HOL
• PVS
• z3
• OpenSMT
• Leon
• CVC4
• RADA
• MoCHi
• Guardol

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
• Recursive proofs for inductive tree data-structures
• Dafny: An Automatic Program Verifier for Functional Correctness
• Towards Complete Reasoning about Axiomatic Specifications
• Sets with Cardinality Constraints in Satisfiability Modulo Theories
• Reasoning About Recursively Defined Data Structures
• Induction for SMT Solvers
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Decision procedures for algebraic data types with abstractions
• Automated Reasoning
• Decidable logics combining heap structures and data