:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Eilers, Marco, Schwerhoff, Malte, Müller, Peter
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	https://arxiv.org/abs/2405.10661
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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

Formal Foundations for Translational Separation Logic Verifiers (extended version)
by: Dardinier, Thibault, et al.
Published: (2024)

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language (extended version)
by: Parthasarathy, Gaurav, et al.
Published: (2024)

Hyper Separation Logic (extended version)
by: Gospodinov, Trayan, et al.
Published: (2026)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

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

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
by: Giunti, Marco, et al.
Published: (2025)

End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation
by: Wu, Jinhua, et al.
Published: (2025)

Protocols to Code: Formal Verification of a Next-Generation Internet Router
by: Pereira, João C., et al.
Published: (2024)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
by: Faella, Marco, et al.
Published: (2024)

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
by: Haselwarter, Philipp G., et al.
Published: (2026)

Context-Aware Separation Logic
by: Meyer, Roland, et al.
Published: (2023)

Automated Verification of Soundness of DNN Certifiers
by: Singh, Avaljot, et al.
Published: (2025)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
by: Rinard, Martin
Published: (2026)

Recursive Mutexes in Separation Logic
by: Du, Ke, et al.
Published: (2026)

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

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

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
by: Foo, Darius, et al.
Published: (2023)

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

Towards Concurrent Quantitative Separation Logic
by: Fesefeldt, Ira, et al.
Published: (2022)

Structural Temporal Logic for Mechanized Program Verification
by: Ioannidis, Eleftherios, et al.
Published: (2024)

FO-Complete Program Verification for Heap Logics
by: Murali, Adithya, et al.
Published: (2026)

Agentic Separation Logic Specification Synthesis
by: Suresh, Tarun, et al.
Published: (2026)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
by: Xu, Qiyuan, et al.
Published: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
by: Mukherjee, Prasita, et al.
Published: (2024)

Automated Software Verification of Hyperliveness
by: Beutner, Raven
Published: (2024)

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

Tunable Automation in Automated Program Verification
by: Bai, Alexander Y., et al.
Published: (2025)

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

Foundational Verification of Smart Contracts through Verified Compilation
by: Sjöberg, Vilhelm, et al.
Published: (2024)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

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

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

Bayesian Separation Logic
by: Ho, Shing Hin, et al.
Published: (2025)

Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions
by: Elad, Neta, et al.
Published: (2025)

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version)
by: Yan, Pengbo, et al.
Published: (2024)

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
by: Ramananandro, Tahina, et al.
Published: (2025)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

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