Bridging arrays and ADTs in recursive proofs

DOI10.1007/978-3-030-72013-1_2MaRDI QIDQ2233489zbMATH OpenOpenAlexFDO

Authors Grigory Fedyukovich, Gidon Ernst

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

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

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)

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

Cites work

• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 1088217 (Why is no real title available?)
• A constructive approach to the problem of program correctness
• Automated discovery of simulation between programs
• Automating induction for solving Horn clauses
• Continuous reasoning: scaling the impact of formal methods
• Data Refinement
• Decision procedures for algebraic data types with abstractions
• Exploiting synchrony and symmetry in relational verification
• HoIce: an ICE-based non-linear Horn clause solver
• Induction for SMT solvers
• Inference rules for proving the equivalence of recursive procedures
• Learning inductive invariants by sampling from frequency distributions
• Modeling in Event B. System and software engineering.
• Program development by stepwise refinement
• Refinement Calculus
• Regression verification for unbalanced recursive functions
• SMT-based model checking for recursive programs
• Solving Horn clauses on inductive data types without induction
• Synthesis of recursive ADT transformations from reusable templates
• The ASM refinement method

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)