Copertina

Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems

Fuente: arXiv

Salvato in:

Dettagli Bibliografici
Autori principali:	Nagar, Kartik, Mukherjee, Prasita, Jagannathan, Suresh
Natura:	Preprint
Pubblicazione:	2020
Soggetti:	Programming Languages
Accesso online:	Acceder al recurso
Tags:	Aggiungi Tag Nessun Tag, puoi essere il primo ad aggiungerne!!

Documenti analoghi

Towards Automated Verification of LLM-Synthesized C Programs
di: Mukherjee, Prasita, et al.
Pubblicazione: (2024)

KestRel: Relational Verification Using E-Graphs for Program Alignment
di: Dickerson, Robert, et al.
Pubblicazione: (2024)

Automatically Verifying Replication-aware Linearizability
di: Soundarapandian, Vimala, et al.
Pubblicazione: (2025)

Liquid Tree Automata
di: Mishra, Ashish, et al.
Pubblicazione: (2026)

Type-Based Incorrectness Reasoning
di: Zhou, Zhe, et al.
Pubblicazione: (2025)

Close is Good Enough: Component-Based Synthesis Modulo Logical Similarity
di: Mishra, Ashish, et al.
Pubblicazione: (2025)

Polymorphic Coverage Types
di: Zhou, Zhe, et al.
Pubblicazione: (2023)

Trace-Guided Synthesis of Effectful Test Generators
di: Zhou, Zhe, et al.
Pubblicazione: (2026)

CIR+CVN: Bridging LLM Semantic Understanding and Petri-Net Verification for Concurrent Programs
di: Zhang, Kaiwen, et al.
Pubblicazione: (2026)

From Traces to Program Incorrectness: A Type-Theoretic Approach
di: Yuan, Yongwei, et al.
Pubblicazione: (2025)

We've Got You Covered: Type-Guided Repair of Incomplete Input Generators
di: LaFontaine, Patrick, et al.
Pubblicazione: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
di: Le, Quang Loc
Pubblicazione: (2025)

Verification of the Release-Acquire Semantics
di: Abdulla, Parosh, et al.
Pubblicazione: (2025)

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

Derivative-Guided Symbolic Execution
di: Yuan, Yongwei, et al.
Pubblicazione: (2024)

Denotational Semantics for Probabilistic and Concurrent Programs
di: Zilberstein, Noam, et al.
Pubblicazione: (2025)

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

Hiord#: An Approach to the Specification and Verification of Higher-Order (C)LP Programs
di: Ciccalè, Marco, et al.
Pubblicazione: (2025)

ConstraintFlow: A DSL for Specification and Verification of Neural Network Analyses
di: Singh, Avaljot, et al.
Pubblicazione: (2024)

Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
di: Redmond, Patrick, et al.
Pubblicazione: (2025)

OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification
di: Li, Shangyu, et al.
Pubblicazione: (2025)

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

Interaction Tree Semantics for RISC-V: Bridging Compiler and Hardware Verification
di: Kan, Shuanglong, et al.
Pubblicazione: (2026)

Agentic Separation Logic Specification Synthesis
di: Suresh, Tarun, et al.
Pubblicazione: (2026)

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
di: Li, Kwing Hei, et al.
Pubblicazione: (2025)

Reduction for Structured Concurrent Programs
di: Gangamreddypalli, Namratha, et al.
Pubblicazione: (2026)

Conversational Concurrency with Dataspaces and Facets
di: Caldwell, Sam, et al.
Pubblicazione: (2025)

Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
di: Fukuda, Kota, et al.
Pubblicazione: (2025)

VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints
di: He, Yang, et al.
Pubblicazione: (2024)

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

Logical Relations for Session-Typed Concurrency
di: Balzer, Stephanie, et al.
Pubblicazione: (2023)

Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis
di: Wei, Anjiang, et al.
Pubblicazione: (2025)

Unfolding Iterators: Specification and Verification of Higher-Order Iterators, in OCaml
di: Chirica, Ion, et al.
Pubblicazione: (2025)

SpecLoop: An Agentic RTL-to-Specification Framework with Formal Verification Feedback Loop
di: Chang, Fu-Chieh, et al.
Pubblicazione: (2026)

The Formal Semantics and Implementation of a Domain-Specific Language for Mixed-Initiative Dialogs
di: Rowland, Zachary S., et al.
Pubblicazione: (2025)

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

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

A Brief Survey of Formal Models of Concurrency
di: Averill, Charles
Pubblicazione: (2024)

Formal Verification for JavaScript Regular Expressions: a Proven Semantics and its Applications (Extended Version)
di: Barrière, Aurèle, et al.
Pubblicazione: (2025)

Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
di: Ball, Thomas, et al.
Pubblicazione: (2024)