Automated synthesis of induction axioms for programs with second-order recursion

DOI10.1007/978-3-642-14203-1_23MaRDI QIDQ5747766zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Automated termination analysis for programs with second-order recursion
• scientific article; zbMATH DE number 108494
• Automated synthesis of recursive programs from a logical specification
• scientific article; zbMATH DE number 3880144
• On automating the extraction of programs from proofs using product types

Cites work

• A Mechanical Proof of the Unsolvability of the Halting Problem
• All-Termination(T)
• An introduction to mathematical logic and type theory: To truth through proof.
• Automated termination analysis for programs with second-order recursion
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 1324445 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)

Cited in

(3)

• Second-order programs with preconditions
• Automated termination analysis for programs with second-order recursion
• scientific article; zbMATH DE number 1341622 (Why is no real title available?)

Describes a project that uses

Uses Software

• ACL2
• Isabelle
• ETPS

This page was built for publication: Automated synthesis of induction axioms for programs with second-order recursion

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