Image de couverture de livre

Relational Hoare Logic for Realistically Modelled Machine Code

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Mazzucato, Denis, Mohamed, Abdalrhman, Lee, Juneyoung, Barrett, Clark, Grundy, Jim, Harrison, John, Pasareanu, Corina S.
Format:	Preprint
Publié:	2025
Sujets:	Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

A Generalized Hybrid Hoare Logic
par: Zhan, Naijun, et autres
Publié: (2023)

On the Relative Completeness of Satisfaction-based Quantum Hoare Logic
par: Sun, Xin, et autres
Publié: (2024)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
par: Mohamed, Abdalrhman, et autres
Publié: (2025)

Access Hoare Logic
par: Beckmann, Arnold, et autres
Publié: (2025)

Relational semantics for flat Heyting-Lewis Logic
par: de Groot, Jim, et autres
Publié: (2026)

A Hoare Logic for Domain Specification (Full Version)
par: Kamburjan, Eduard, et autres
Publié: (2024)

Complete Quantum Relational Hoare Logics from Optimal Transport Duality
par: Barthe, Gilles, et autres
Publié: (2025)

On the Relative Completeness of Satisfaction-based Probabilistic Hoare Logic With While Loop
par: Sun, Xin, et autres
Publié: (2024)

Cyclic Proofs in Hoare Logic and its Reverse
par: Brotherston, James, et autres
Publié: (2025)

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
par: Dardinier, Thibault, et autres
Publié: (2023)

Verifying SQL Queries using Theories of Tables and Relations
par: Mohamed, Mudathir, et autres
Publié: (2024)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
par: Zimmerman, Conrad, et autres
Publié: (2024)

Continuation Semantics for Fixpoint Modal Logic and Computation Tree Logics
par: Kojima, Ryota, et autres
Publié: (2025)

Automatic Function Annotations for Hoare Logic
par: Matichuk, Danielle
Publié: (2012)

CSLib: The Lean Computer Science Library
par: Barrett, Clark, et autres
Publié: (2026)

A quantitative probabilistic relational Hoare logic
par: Avanzini, Martin, et autres
Publié: (2024)

A Practical Quantum Hoare Logic with Classical Variables, I
par: Ying, Mingsheng
Publié: (2024)

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason
par: de Groot, Jim, et autres
Publié: (2026)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK
par: de Groot, Jim, et autres
Publié: (2024)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
par: Powell, Thomas
Publié: (2023)

Alignment complete relational Hoare logics for some and all
par: Nagasamudram, Ramana, et autres
Publié: (2023)

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs
par: Rao, Balaji, et autres
Publié: (2026)

The nonexistence of unicorns and many-sorted Löwenheim-Skolem theorems
par: Przybocki, Benjamin, et autres
Publié: (2024)

Relative Completeness of Incorrectness Separation Logic
par: Lee, Yeonseok, et autres
Publié: (2025)

A General (Uniform) Relational Semantics for Sentential Logics
par: Hartonas, Chrysafis
Publié: (2025)

Cubing for Tuning
par: Wu, Haoze, et autres
Publié: (2025)

Satisfiability Modulo Extensional Constant Arrays (Extended Version)
par: Preiner, Mathias, et autres
Publié: (2026)

Generalized Optimization Modulo Theories
par: Tsiskaridze, Nestan, et autres
Publié: (2024)

A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
par: Verscht, Lena, et autres
Publié: (2024)

Solving Set Constraints with Comprehensions and Bounded Quantifiers
par: Mohamed, Mudathir, et autres
Publié: (2025)

Positive First-order Logic on Words and Graphs
par: Kuperberg, Denis
Publié: (2022)

A Logic of Secrecy on Simplicial Models
par: Wang, Shanxia
Publié: (2026)

Intuitionistic monotone modal logic via translation
par: de Groot, Jim
Publié: (2025)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
par: Qian, Yicheng, et autres
Publié: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
par: Pertseva, Elizaveta, et autres
Publié: (2026)

Linear-time logics -- a coalgebraic perspective
par: Cirstea, Corina
Publié: (2016)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
par: Oda, Yukihiro
Publié: (2025)

Agent-Knowledge Logic for Alternative Epistemic Logic
par: Nishimura, Yuki
Publié: (2024)

A foundational characterization of Hoare Logic
par: Leivant, Daniel
Publié: (2026)

On The Metric Nature of (Differential) Logical Relations
par: Lago, Ugo Dal, et autres
Publié: (2025)