Tactical theorem proving in program verification

DOI10.1007/3-540-52885-7_83MaRDI QIDQ6488526zbMATH OpenFDO

Authors Michael Heisel, Wolfgang Reif, Werner Stephan

Publication date 28 April 2023

Full work available at URL https://doi.org/10.1007/3-540-52885-7_83

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Axiomatising the logic of computer programming
• Edinburgh LCF. A mechanized logic of computation
• First-order dynamic logic
• scientific article; zbMATH DE number 3870631 (Why is no real title available?)
• scientific article; zbMATH DE number 4024753 (Why is no real title available?)
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 4101151 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 3740740 (Why is no real title available?)
• scientific article; zbMATH DE number 3469999 (Why is no real title available?)
• scientific article; zbMATH DE number 194783 (Why is no real title available?)
• Logic and Computation
• Proving program inclusion using Hoare's logic

Cited in

(15)

• Reuse of proofs in software verification
• Planning from second principles
• Programmed strategies for program verification
• Ensuring the correctness of lightweight tactics for JavaCard dynamic logic
• scientific article; zbMATH DE number 2177623 (Why is no real title available?)
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• scientific article; zbMATH DE number 4074539 (Why is no real title available?)
• scientific article; zbMATH DE number 107898 (Why is no real title available?)
• scientific article; zbMATH DE number 827984 (Why is no real title available?)
• Studying a Range Proof Technique — Exception and Optimisation
• One logic to use them all
• Tactic theorem proving with refinement-tree proofs and metavariables
• \textit{Mollusc}: a general proof-development shell for sequent-based logics
• Logics in Artificial Intelligence
• Computer Aided Verification

This page was built for publication: Tactical theorem proving in program verification

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