Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion

DOI10.1007/978-3-642-14203-1_23zbMath1291.68316OpenAlexW1523149815MaRDI QIDQ5747766

Markus Aderhold

Publication date: 14 September 2010

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

Full work available at URL: https://doi.org/10.1007/978-3-642-14203-1_23

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

Second-Order Programs with Preconditions

Uses Software

• ACL2
• Isabelle
• ETPS

Cites Work

• An introduction to mathematical logic and type theory: To truth through proof.
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Automated Termination Analysis for Programs with Second-Order Recursion
• All-Termination(T)
• A Mechanical Proof of the Unsolvability of the Halting Problem
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion