Imagen de Portada

Automatically Verifying Replication-aware Linearizability

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Soundarapandian, Vimala, Nagar, Kartik, Rastogi, Aseem, Sivaramakrishnan, KC
Formato:	Preprint
Publicado:	2025
Materias:	Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Sal: Multi-modal Verification of Replicated Data Types
por: Ramesh, Pranav, et al.
Publicado: (2026)

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
por: Nagar, Kartik, et al.
Publicado: (2020)

Efficient Linearizability Monitoring
por: Abdulla, Parosh Aziz, et al.
Publicado: (2025)

Enabling Memory Safety of C Programs using LLMs
por: Mohammed, Nausheen, et al.
Publicado: (2024)

Fixed Parameter Tractable Linearizability Monitoring
por: Han, Lee Zheng, et al.
Publicado: (2025)

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
por: Kent, Zachary, et al.
Publicado: (2025)

Efficient Decrease-and-Conquer Linearizability Monitoring
por: Han, Lee Zheng, et al.
Publicado: (2024)

Ranking LLM-Generated Loop Invariants for Program Verification
por: Chakraborty, Saikat, et al.
Publicado: (2023)

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

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
por: Wu, Jinhua, et al.
Publicado: (2026)

Verified Code Transpilation with LLMs
por: Bhatia, Sahil, et al.
Publicado: (2024)

Verified Parameterized Choreographies Technical Report
por: Rubbens, Robert, et al.
Publicado: (2025)

Increasing the Expressiveness of a Gradual Verifier
por: Gupta, Priyam
Publicado: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
por: Jamner, Dustin, et al.
Publicado: (2025)

MAG$π$!: The Role of Replication in Typing Failure-Prone Communication
por: Brun, Matthew Alan Le, et al.
Publicado: (2024)

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
por: Pezeshkpour, Pouya, et al.
Publicado: (2026)

Dependent Session Types for Verified Concurrent Programming
por: Fu, Qiancheng, et al.
Publicado: (2025)

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

Verifying Sequential Consistency under Bounded Preemptions
por: Govind, R., et al.
Publicado: (2026)

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation
por: Yang, Xiaoxiao, et al.
Publicado: (2017)

Caesar: A Deductive Verifier for Probabilistic Programs
por: Schröer, Philipp, et al.
Publicado: (2026)

Crux, a Precise Verifier for Rust and Other Languages
por: Pernsteiner, Stuart, et al.
Publicado: (2024)

KATch: A Fast Symbolic Verifier for NetKAT
por: Moeller, Mark, et al.
Publicado: (2024)

A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
por: Zhou, Zhe, et al.
Publicado: (2024)

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

Expanding Specification Capabilities of a Gradual Verifier with Pure Functions
por: Mutlu, Doruk Alp
Publicado: (2025)

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

Toward Verified Library-Level Choreographic Programming with Algebraic Effects
por: Shen, Gan, et al.
Publicado: (2024)

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

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

Strengthening Solidity Invariant Generation: From Post- to Pre-Deployment
por: Kaushik, Kartik, et al.
Publicado: (2024)

Galois Slicing as Automatic Differentiation
por: Atkey, Robert, et al.
Publicado: (2025)

Automatic layout of railroad diagrams
por: Chiplunkar, Shardul, et al.
Publicado: (2025)

Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
por: Tekriwal, Mohit, et al.
Publicado: (2025)

HELIX: Verified compilation of cyber-physical control systems to LLVM IR
por: Zaliva, Vadim, et al.
Publicado: (2026)

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

SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation
por: Nezhad, Sina Bagheri, et al.
Publicado: (2025)

Verifying Correctness of Shared Channels in a Cooperatively Scheduled Process-Oriented Language
por: Pedersen, Jan, et al.
Publicado: (2025)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
por: Fedchin, Aleksandr, et al.
Publicado: (2025)

LoRe: A Programming Model for Verifiably Safe Local-First Software
por: Haas, Julian, et al.
Publicado: (2023)