Copertina

Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Wu, Shushu, Wu, Xiwei, Cao, Qinxiang
Natura:	Preprint
Pubblicazione:	2025
Soggetti:	Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

A Hoare Logic for Symmetry Properties
di: Mehta, Vaibhav, et al.
Pubblicazione: (2025)

Towards Definitional Interpreters for Hoare Logics
di: Sun, Ke, et al.
Pubblicazione: (2026)

Relational Hoare Logic for High-Level Synthesis of Hardware Accelerators
di: Tanaka, Izumi, et al.
Pubblicazione: (2026)

Cyclic Proofs in Hoare Logic and its Reverse
di: Brotherston, James, et al.
Pubblicazione: (2025)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
di: Zimmerman, Conrad, et al.
Pubblicazione: (2024)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
di: Nagy, Shaan, et al.
Pubblicazione: (2024)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
di: Yang, Chengxi, et al.
Pubblicazione: (2025)

A Practical Quantum Hoare Logic with Classical Variables, I
di: Ying, Mingsheng
Pubblicazione: (2024)

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
di: Sundaram, Aarthi, et al.
Pubblicazione: (2021)

A Coq Library of Sets for Teaching Denotational Semantics
di: Cao, Qinxiang, et al.
Pubblicazione: (2024)

Stellis: A Strategy Language for Purifying Separation Logic Entailments
di: Wang, Zhiyi, et al.
Pubblicazione: (2025)

QCP: A Practical Separation Logic-based C Program Verification Tool
di: Wu, Xiwei, et al.
Pubblicazione: (2025)

Access Hoare Logic
di: Beckmann, Arnold, et al.
Pubblicazione: (2025)

On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
di: Sun, Xin, et al.
Pubblicazione: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
di: Verscht, Lena, et al.
Pubblicazione: (2024)

Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation
di: Liu, Chang, et al.
Pubblicazione: (2023)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
di: Oda, Yukihiro
Pubblicazione: (2025)

Relational Hoare Logic for Realistically Modelled Machine Code
di: Mazzucato, Denis, et al.
Pubblicazione: (2025)

A Generalized Hybrid Hoare Logic
di: Zhan, Naijun, et al.
Pubblicazione: (2023)

A foundational characterization of Hoare Logic
di: Leivant, Daniel
Pubblicazione: (2026)

Automatic Function Annotations for Hoare Logic
di: Matichuk, Danielle
Pubblicazione: (2012)

Finding $\forall\exists$ Hyperbugs using Symbolic Execution
di: Correnson, Arthur, et al.
Pubblicazione: (2025)

Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
di: Park, Sewon, et al.
Pubblicazione: (2016)

Complete Quantum Relational Hoare Logics from Optimal Transport Duality
di: Barthe, Gilles, et al.
Pubblicazione: (2025)

On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop
di: Sun, Xin, et al.
Pubblicazione: (2024)

A Hoare Logic for Domain Specification (Full Version)
di: Kamburjan, Eduard, et al.
Pubblicazione: (2024)

Denotation-based Compositional Compiler Verification
di: Cheng, Zhang, et al.
Pubblicazione: (2024)

A Natural Formalized Proof Language
di: Xie, Lihan, et al.
Pubblicazione: (2024)

Logical Relations for Session-Typed Concurrency
di: Balzer, Stephanie, et al.
Pubblicazione: (2023)

Modeling Reachability Types with Logical Relations
di: Bao, Yuyan, et al.
Pubblicazione: (2023)

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
di: Ling, Hongyi, et al.
Pubblicazione: (2026)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
di: Dardinier, Thibault, et al.
Pubblicazione: (2023)

On Computational Indistinguishability and Logical Relations
di: Lago, Ugo Dal, et al.
Pubblicazione: (2024)

From Program Logics to Language Logics
di: Cimini, Matteo
Pubblicazione: (2024)

Tail Modulo Cons, OCaml, and Relational Separation Logic
di: Allain, Clément, et al.
Pubblicazione: (2024)

A Language-Agnostic Logical Relation for Message-Passing Protocols
di: Zhang, Tesla, et al.
Pubblicazione: (2025)

Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
di: Yao, Yue, et al.
Pubblicazione: (2024)

Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
di: Zhang, Tesla, et al.
Pubblicazione: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
di: Gregersen, Simon Oddershede, et al.
Pubblicazione: (2025)

Functional Logic Program Transformations
di: Hanus, Michael, et al.
Pubblicazione: (2026)