Buchumschlag

Verifying Concurrent Stacks by Divergence-Sensitive Bisimulation

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Yang, Xiaoxiao, Katoen, Joost-Pieter, Wu, Hao
Format:	Preprint
Veröffentlicht:	2017
Schlagworte:	Programming Languages
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

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

Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
von: Schröer, Philipp, et al.
Veröffentlicht: (2026)

Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
von: Schröer, Philipp, et al.
Veröffentlicht: (2025)

Caesar: A Deductive Verifier for Probabilistic Programs
von: Schröer, Philipp, et al.
Veröffentlicht: (2026)

Quantifier Elimination and Craig Interpolation, Quantitatively
von: Batz, Kevin, et al.
Veröffentlicht: (2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
von: Batz, Kevin, et al.
Veröffentlicht: (2025)

Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
von: Klinkenberg, Lutz, et al.
Veröffentlicht: (2023)

Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version)
von: Haase, Darion, et al.
Veröffentlicht: (2026)

Unknown Biases and Timing Constraints in Timed Automata
von: Haase, Darion, et al.
Veröffentlicht: (2024)

Dependent Session Types for Verified Concurrent Programming
von: Fu, Qiancheng, et al.
Veröffentlicht: (2025)

A Spectrum of Approximate Probabilistic Bisimulations
von: Spork, Timm, et al.
Veröffentlicht: (2024)

Compactness via Pattern Stepping Bisimulation
von: Scharager, Matias
Veröffentlicht: (2024)

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
von: Spork, Timm, et al.
Veröffentlicht: (2025)

DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs
von: Fedchin, Aleksandr, et al.
Veröffentlicht: (2025)

Model Checking Temporal Properties of Recursive Probabilistic Programs
von: Winkler, Tobias, et al.
Veröffentlicht: (2021)

StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
von: Reitz, Antonin, et al.
Veröffentlicht: (2024)

Sharded Elimination and Combining for Highly-Efficient Concurrent Stacks
von: Singh, Ajay, et al.
Veröffentlicht: (2026)

A Formal Framework for Naturally Specifying and Verifying Sequential Algorithms
von: Yang, Chengxi, 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)

RustCompCert: A Verified and Verifying Compiler for a Sequential Subset of Rust
von: Wu, Jinhua, et al.
Veröffentlicht: (2026)

Verifying Sampling Algorithms via Distributional Invariants
von: Zilken, Daniel, et al.
Veröffentlicht: (2025)

Reduction for Structured Concurrent Programs
von: Gangamreddypalli, Namratha, et al.
Veröffentlicht: (2026)

Conversational Concurrency with Dataspaces and Facets
von: Caldwell, Sam, et al.
Veröffentlicht: (2025)

Logical Relations for Session-Typed Concurrency
von: Balzer, Stephanie, et al.
Veröffentlicht: (2023)

Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
von: Heck, Linus, et al.
Veröffentlicht: (2025)

A Brief Survey of Formal Models of Concurrency
von: Averill, Charles
Veröffentlicht: (2024)

Evaluate the Stack Management in Effect Handlers using the libseff C Library
von: Yu, ZeHao
Veröffentlicht: (2025)

Scenario-Based Proofs for Concurrent Objects [Extended Version]
von: Enea, Constantin, et al.
Veröffentlicht: (2023)

Verified Code Transpilation with LLMs
von: Bhatia, Sahil, et al.
Veröffentlicht: (2024)

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
von: Nagar, Kartik, et al.
Veröffentlicht: (2020)

Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
von: Redmond, Patrick, et al.
Veröffentlicht: (2025)

Verified Parameterized Choreographies Technical Report
von: Rubbens, Robert, et al.
Veröffentlicht: (2025)

Increasing the Expressiveness of a Gradual Verifier
von: Gupta, Priyam
Veröffentlicht: (2025)

Pyrosome: Verified Compilation for Modular Metatheory
von: Jamner, Dustin, et al.
Veröffentlicht: (2025)

Automatically Verifying Replication-aware Linearizability
von: Soundarapandian, Vimala, et al.
Veröffentlicht: (2025)

An Asynchronous Scheme for Rollback Recovery in Message-Passing Concurrent Programming Languages
von: Vidal, Germán
Veröffentlicht: (2023)

Qafny: A Quantum-Program Verifier
von: Li, Liyi, et al.
Veröffentlicht: (2022)

AutoPyVerifier: Learning Compact Executable Verifiers for Large Language Model Outputs
von: Pezeshkpour, Pouya, et al.
Veröffentlicht: (2026)

Verification Algorithms for Automated Separation Logic Verifiers
von: Eilers, Marco, et al.
Veröffentlicht: (2024)

Verifying Sequential Consistency under Bounded Preemptions
von: Govind, R., et al.
Veröffentlicht: (2026)