Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
From MaRDI portal
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)
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)
