Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding

DOI10.1007/S10817-024-09706-5MaRDI QIDQ6611968zbMATH OpenFDO

Authors Zhongye Wang, Qinxiang Cao, Yichen Tao

Publication date 27 September 2024

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

Full work available at URL https://doi.org/10.1007/S10817-024-09706-5

zbMATH Keywords

deep embeddingHoare logicmachine-checked proofsprogram verificationseparation logicshallow embedding

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A lattice-theoretical fixpoint theorem and its applications
• A semantics for concurrent separation logic
• AUTO2, a saturation-based heuristic prover for higher-order logic
• Axiomatic approach to total correctness of programs
• Beweisstudien zum Satz von M. Zorn. Herrn Erhard. Schmidt zum 75. Geburtstag gewidmet
• Certified assembly programming with embedded code pointers
• Characteristic formulae for the verification of imperative programs
• CSimpl: a rely-guarantee-based framework for verifying concurrent programs
• Dijkstra and Hoare monads in monadic computation
• Dijkstra monads for free
• Hoare type theory, polymorphism and separation
• scientific article; zbMATH DE number 1956565 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Precision and the conjunction rule in concurrent separation logic
• Program verification through characteristic formulae
• Separation and information hiding
• Soundness and Completeness of an Axiom System for Program Verification
• Sur le théorème de Zorn
• Theorem Proving in Higher Order Logics
• Verified characteristic formulae for CakeML
• Verified software toolchain (invited talk)
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• VST-Floyd: a separation logic tool to verify correctness of C programs
• Ynot: dependent types for imperative programs

Cited in

(2)

• Faithful logic embeddings in HOL -- deep and shallow
• Faithful Logic Embeddings in HOL — Deep and Shallow (Isabelle/HOL dataset)

This page was built for publication: Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding

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