Buchumschlag

Verification Algorithms for Automated Separation Logic Verifiers

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Eilers, Marco, Schwerhoff, Malte, Müller, Peter
Format:	Preprint
Veröffentlicht:	2024
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)
von: Ling, Hongyi, et al.
Veröffentlicht: (2026)

Formal Foundations for Translational Separation Logic Verifiers (extended version)
von: Dardinier, Thibault, et al.
Veröffentlicht: (2024)

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

Hyper Separation Logic (extended version)
von: Gospodinov, Trayan, et al.
Veröffentlicht: (2026)

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

Compositional Verification in Concurrent Separation Logic with Permissions Regions
von: Le, Quang Loc
Veröffentlicht: (2025)

QCP: A Practical Separation Logic-based C Program Verification Tool
von: Wu, Xiwei, et al.
Veröffentlicht: (2025)

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

Iso-Recursive Multiparty Sessions and their Automated Verification -- Technical Report
von: Giunti, Marco, et al.
Veröffentlicht: (2025)

Automated Verification of Tree-Manipulating Programs Using Constrained Horn Clauses
von: Faella, Marco, et al.
Veröffentlicht: (2024)

Context-Aware Separation Logic
von: Meyer, Roland, et al.
Veröffentlicht: (2023)

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

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

Automated Verification of Soundness of DNN Certifiers
von: Singh, Avaljot, et al.
Veröffentlicht: (2025)

Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
von: Rinard, Martin
Veröffentlicht: (2026)

Tail Modulo Cons, OCaml, and Relational Separation Logic
von: Allain, Clément, et al.
Veröffentlicht: (2024)

Staged Specification Logic for Verifying Higher-Order Imperative Programs (Technical Report)
von: Foo, Darius, et al.
Veröffentlicht: (2023)

Recursive Mutexes in Separation Logic
von: Du, Ke, et al.
Veröffentlicht: (2026)

Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
von: Zimmerman, Conrad, et al.
Veröffentlicht: (2024)

Towards Automated Verification of LLM-Synthesized C Programs
von: Mukherjee, Prasita, et al.
Veröffentlicht: (2024)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
von: Yang, Chengxi, et al.
Veröffentlicht: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
von: Gregersen, Simon Oddershede, et al.
Veröffentlicht: (2025)

Towards Concurrent Quantitative Separation Logic
von: Fesefeldt, Ira, et al.
Veröffentlicht: (2022)

Structural Temporal Logic for Mechanized Program Verification
von: Ioannidis, Eleftherios, et al.
Veröffentlicht: (2024)

FO-Complete Program Verification for Heap Logics
von: Murali, Adithya, et al.
Veröffentlicht: (2026)

Automated Software Verification of Hyperliveness
von: Beutner, Raven
Veröffentlicht: (2024)

Agentic Separation Logic Specification Synthesis
von: Suresh, Tarun, et al.
Veröffentlicht: (2026)

A Nominal Approach to Probabilistic Separation Logic
von: Li, John M., et al.
Veröffentlicht: (2024)

Tunable Automation in Automated Program Verification
von: Bai, Alexander Y., et al.
Veröffentlicht: (2025)

Automated Theorem Proving for Prolog Verification
von: Mesnard, Fred, et al.
Veröffentlicht: (2026)

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

Stellis: A Strategy Language for Purifying Separation Logic Entailments
von: Wang, Zhiyi, et al.
Veröffentlicht: (2025)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
von: Xu, Qiyuan, et al.
Veröffentlicht: (2024)

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

Reasoning about Weak Isolation Levels in Separation Logic
von: Mathiasen, Anders Alnor, et al.
Veröffentlicht: (2025)

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
von: Nagy, Shaan, et al.
Veröffentlicht: (2024)

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

Secure Parsing and Serializing with Separation Logic Applied to CBOR, CDDL, and COSE
von: Ramananandro, Tahina, et al.
Veröffentlicht: (2025)

Automated Formal Verification of a Software Fault Isolation System
von: Sotoudeh, Matthew, et al.
Veröffentlicht: (2025)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
von: Haselwarter, Philipp G., et al.
Veröffentlicht: (2024)