Bridging arrays and ADTs in recursive proofs

DOI10.1007/978-3-030-72013-1_2zbMATH Open1474.68048OpenAlexW3136078500MaRDI QIDQ2233489FDOQ2233489

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

Recommendations

• Relational verification via invariant-guided synchronization
• Data abstraction: a general framework to handle program verification of data structures
• Inference rules for proving the equivalence of recursive procedures
• Invariant Synthesis for Combined Theories
• Symbolic automatic relations and their applications to SMT and CHC solving

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233489)