Imagen de Portada

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

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Wu, Shushu, Wu, Xiwei, Cao, Qinxiang
Formato:	Preprint
Publicado:	2025
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

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

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

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

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

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

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

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

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

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

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

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

Access Hoare Logic
por: Beckmann, Arnold, et al.
Publicado: (2025)

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

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

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

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
por: Oda, Yukihiro
Publicado: (2025)

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

A Generalized Hybrid Hoare Logic
por: Zhan, Naijun, et al.
Publicado: (2023)

A foundational characterization of Hoare Logic
por: Leivant, Daniel
Publicado: (2026)

Automatic Function Annotations for Hoare Logic
por: Matichuk, Danielle
Publicado: (2012)

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

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

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

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

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

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

A Natural Formalized Proof Language
por: Xie, Lihan, et al.
Publicado: (2024)

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

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

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

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

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

From Program Logics to Language Logics
por: Cimini, Matteo
Publicado: (2024)

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

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

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

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

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

Functional Logic Program Transformations
por: Hanus, Michael, et al.
Publicado: (2026)