:: Library Catalog

Cover Image

Saved in:

Bibliographic Details
Main Authors:	Dardinier, Thibault, Sammler, Michael, Parthasarathy, Gaurav, Summers, Alexander J., Müller, Peter
Format:	Preprint
Published:	2024
Subjects:	Programming Languages
Online Access:	https://arxiv.org/abs/2407.20002
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

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)

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

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

Verification Algorithms for Automated Separation Logic Verifiers
by: Eilers, Marco, et al.
Published: (2024)

HITrees: Higher-Order Interaction Trees
by: Ayyam, Amir Mohammad Fadaei, et al.
Published: (2025)

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

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

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
by: Poli, Federico, et al.
Published: (2024)

Resource Specifications for Resource-Manipulating Programs
by: Grannan, Zachary, et al.
Published: (2023)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

Formally Verified Linear-Time Invertible Lexing
by: Chassot, Samuel, et al.
Published: (2025)

Reactive graphs in action (extended version)
by: Tinoco, David, et al.
Published: (2024)

The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)
by: Arquint, Linard, et al.
Published: (2025)

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

Relaxed exception semantics for Arm-A (extended version)
by: Simner, Ben, et al.
Published: (2024)

Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
by: Grannan, Zachary, et al.
Published: (2025)

From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs
by: Cao, Jialun, et al.
Published: (2025)

Minuska: Towards a Formally Verified Programming Language Framework
by: Tušil, Jan, et al.
Published: (2024)

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

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
by: Ravi, Nikil, et al.
Published: (2026)

Formally Verified C Code Generation from Hybrid Communicating Sequential Processes
by: Wang, Shuling, et al.
Published: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts
by: Huyghebaert, Sander, et al.
Published: (2023)

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)

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

A Formally Verified Robustness Certifier for Neural Networks (Extended Version)
by: Tobler, James, et al.
Published: (2025)

Triosecuris: Formally Verified Protection Against Speculative Control-Flow Hijacking
by: Baumann, Jonathan, et al.
Published: (2026)

Nanopass Back-Translation of Call-Return Trees for Mechanized Secure Compilation Proofs
by: Thibault, Jérémy, et al.
Published: (2025)

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

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

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study
by: Bucev, Mario, et al.
Published: (2024)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
by: Reitz, Antonin, et al.
Published: (2024)

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

Picachv: Formally Verified Data Use Policy Enforcement for Secure Data Analytics
by: Chen, Haobin Hiroki, et al.
Published: (2025)

VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
by: Zeng, Lingfei, et al.
Published: (2025)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
by: Ileri, Atalay Mert, et al.
Published: (2024)

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