Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
From MaRDI portal
Publication:6611968
DOI10.1007/S10817-024-09706-5MaRDI QIDQ6611968
Could not fetch data.
Publication date: 27 September 2024
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Hoare logicseparation logicprogram verificationdeep embeddingshallow embeddingmachine-checked proofs
Cites Work
- Title not available (Why is that?)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- A semantics for concurrent separation logic
- Dijkstra and Hoare monads in monadic computation
- Isabelle. A generic theorem prover
- Isabelle/HOL. A proof assistant for higher-order logic
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Axiomatic approach to total correctness of programs
- Sur le théorème de Zorn
- A lattice-theoretical fixpoint theorem and its applications
- AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic
- Verified Characteristic Formulae for CakeML
- Verified Software Toolchain
- CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
- Separation and information hiding
- Imperative Functional Programming with Isabelle/HOL
- Hoare type theory, polymorphism and separation
- Soundness and Completeness of an Axiom System for Program Verification
- Iris from the ground up: A modular foundation for higher-order concurrent separation logic
- Program verification through characteristic formulae
- Characteristic formulae for the verification of imperative programs
- Ynot
- Certified assembly programming with embedded code pointers
- Dijkstra monads for free
- Theorem Proving in Higher Order Logics
- Precision and the Conjunction Rule in Concurrent Separation Logic
- Beweisstudien zum Satz von M. Zorn. Herrn Erhard. Schmidt zum 75. Geburtstag gewidmet
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)
