Bridging arrays and ADTs in recursive proofs

DOI10.1007/978-3-030-72013-1_2zbMath1474.68048OpenAlexW3136078500MaRDI QIDQ2233489

Gidon Ernst, Grigory Fedyukovich

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_2

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Symbolic automatic relations and their applications to SMT and CHC solving ⋮ Solving constrained Horn clauses over algebraic data types

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SMT-based model checking for recursive programs
• The ASM refinement method
• Inference rules for proving the equivalence of recursive procedures
• Automating induction for solving Horn clauses
• Learning inductive invariants by sampling from frequency distributions
• Regression verification for unbalanced recursive functions
• Synthesis of Recursive ADT Transformations from Reusable Templates
• Automated Discovery of Simulation Between Programs
• Refinement Calculus
• Solving Horn Clauses on Inductive Data Types Without Induction
• Data Refinement
• Continuous Reasoning
• Induction for SMT Solvers
• Decision procedures for algebraic data types with abstractions
• A constructive approach to the problem of program correctness
• Program development by stepwise refinement
• Exploiting synchrony and symmetry in relational verification
• HoIce: an ICE-based non-linear Horn clause solver

This page was built for publication: Bridging arrays and ADTs in recursive proofs