Image de couverture de livre

Verifying Lock-free Search Structure Templates

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Patel, Nisarg, Shasha, Dennis, Wies, Thomas
Format:	Preprint
Publié:	2024
Sujets:	Programming Languages 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

Logical Relations for Formally Verified Authenticated Data Structures
par: Gregersen, Simon Oddershede, et autres
Publié: (2025)

Verifying Solutions to Semantics-Guided Synthesis Problems
par: Murphy, Charlie, et autres
Publié: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
par: Monniaux, David
Publié: (2024)

Breaking the Mold: Nonlinear Ranking Function Synthesis Without Templates
par: Zhu, Shaowei, et autres
Publié: (2024)

Verifying Floating-Point Programs in Stainless
par: Gilot, Andrea, et autres
Publié: (2026)

Verifying Peephole Rewriting In SSA Compiler IRs
par: Bhat, Siddharth, et autres
Publié: (2024)

Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
par: Sulzmann, Martin
Publié: (2026)

Sound and Complete Witnesses for Template-based Verification of LTL Properties on Polynomial Programs
par: Chatterjee, Krishnendu, et autres
Publié: (2024)

Verifying Functional Correctness Properties At the Level of Java Bytecode
par: Paganoni, Marco, et autres
Publié: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
par: Wang, Keyin, et autres
Publié: (2026)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
par: Coglio, Alessandro, et autres
Publié: (2025)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
par: de Vilhena, Paulo Emílio, et autres
Publié: (2021)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
par: Grandury, Marcos, et autres
Publié: (2025)

Zippy -- Generic White-Box Proof Search with Zippers
par: Kappelmann, Kevin
Publié: (2025)

A Complete Inference System for Skip-free Guarded Kleene Algebra with Tests
par: Kappé, Tobias, et autres
Publié: (2023)

Verifying Asynchronous Hyperproperties in Reactive Systems
par: Beutner, Raven, et autres
Publié: (2025)

Monoid Structures on Indexed Containers
par: De Pascalis, Michele, et autres
Publié: (2025)

Structural Analysis of GRAFCET Control Specifications
par: Schnakenbeck, Aron, et autres
Publié: (2023)

Structural Temporal Logic for Mechanized Program Verification
par: Ioannidis, Eleftherios, et autres
Publié: (2024)

VEL: A Formally Verified Reasoner for OWL2 EL Profile
par: Ileri, Atalay Mert, et autres
Publié: (2024)

Automated Verification of Monotonic Data Structure Traversals in C
par: Sotoudeh, Matthew
Publié: (2025)

Mechanised Hypersafety Proofs about Structured Data: Extended Version
par: Gladshtein, Vladimir, et autres
Publié: (2024)

An Introduction to Different Approaches to Initial Semantics
par: Lamiaux, Thomas, et autres
Publié: (2024)

Expressivity of AuDaLa: Turing Completeness and Possible Extensions
par: Franken, Tom T. P., et autres
Publié: (2024)

Verified Purely Functional Catenable Real-Time Deques
par: Viennot, Jules, et autres
Publié: (2025)

Unrealizability Logic
par: Kim, Jinwoo, et autres
Publié: (2022)

Towards Concurrent Quantitative Separation Logic
par: Fesefeldt, Ira, et autres
Publié: (2022)

Kleene algebra with commutativity conditions is undecidable
par: de Amorim, Arthur Azevedo, et autres
Publié: (2024)

Can Proof Assistants Verify Multi-Agent Systems?
par: Mendez, Julian Alfredo, et autres
Publié: (2025)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
par: Kaye, George
Publié: (2025)

Impredicativity in Linear Dependent Type Theory
par: Speight, Sam, et autres
Publié: (2026)

Evaluating the Ability of Large Language Models to Generate Verifiable Specifications in VeriFast
par: Fan, Wen, et autres
Publié: (2024)

More Church-Rosser Proofs in BELUGA
par: Momigliano, Alberto, et autres
Publié: (2024)

Bialgebraic Reasoning on Higher-Order Program Equivalence
par: Goncharov, Sergey, et autres
Publié: (2024)

A Nominal Approach to Probabilistic Separation Logic
par: Li, John M., et autres
Publié: (2024)

Syntax-Guided Automated Program Repair for Hyperproperties
par: Beutner, Raven, et autres
Publié: (2024)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
par: Hu, Jason Z. S., et autres
Publié: (2024)

Hybrid Intersection Types for PCF (Extended Version)
par: Barenbaum, Pablo, et autres
Publié: (2024)

Functional Array Programming in an Extended Pi-Calculus
par: Hüttel, Hans, et autres
Publié: (2024)

An Abstract Domain for Heap Commutativity (Extended Version)
par: Pincus, Jared, et autres
Publié: (2024)