Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
From MaRDI portal
- \textsc{SecCSL}: security concurrent separation logic
- A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs
- An assertion-based program logic for probabilistic programs
- An axiomatic basis for computer programming
- Beyond 2-safety: asymmetric product programs for relational program verification
- First-order dynamic logic
- Formal certification of code-based cryptographic proofs
- Guarded commands, nondeterminacy and formal derivation of programs
- Hoare logic and auxiliary variables
- Unnamed Publication
- Unnamed Publication
- Hypercollecting semantics and its application to static analysis of information flow
- Isabelle/HOL. A proof assistant for higher-order logic
- Local reasoning about the presence of bugs: incorrectness separation logic
- On algebra of program correctness and incorrectness
- Product properties and their direct verification
- Propositional Dynamic Logic for Hyperproperties
- Relational separation logic
- Resources, concurrency, and local reasoning
- Reverse Hoare logic
- Secure information flow by self-composition
- Simple relational correctness proofs for static analyses and program transformations
- Software Verification of Hyperproperties Beyond k-Safety
- Static Analysis
- The existence of refinement mappings
- Verifying hyperliveness
- VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC
This page was built for software: Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
