VYRD: verifYing concurrent programs by runtime refinement-violation detection

No abstract is available for this paper.

• Publication year

  2005

• Venue

  ACM-SIGPLAN Symposium on Programming Language Design and Implementation

• Publication date

  2005-06-12

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1065010.1065015
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Runtime Refinement Checking of Concurrent Data Structures

  2004cited by this paper
• Atomizer: a dynamic atomicity checker for multithreaded programs

  2004cited by this paper
• Boxwood: Abstractions as the Foundation for Storage Infrastructure

  2004cited by this paper
• Verifying Commit-Atomicity Using Model-Checking

  2004influential reference
• Exploiting purity for atomicity

  2004cited by this paper
• Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

  2003cited by this paper
• A type and effect system for atomicity

  2003cited by this paper
• Types for atomicity

  2003influential reference
• Using a formal specification and a model checker to monitor and direct simulation

  2003cited by this paper
• Runtime Conformance Checking of Objects Using Alloy

  2003cited by this paper
• Run-Time Analysis for Atomicity

  2003influential reference
• Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions

  1998cited by this paper
• Linearizability: a correctness condition for concurrent objects

  1990cited by this paper
• The existence of refinement mappings

  1988cited by this paper
• Concurrent operations on B-trees with overtaking

  1985cited by this paper

• Asynchronous Fault-Tolerant Language Decidability for Runtime Verification of Distributed Systems

  2025cites this paper
• Multi-Grained Specifications for Distributed System Model Checking and Verification

  2024influential citation
• Asynchronous Wait-Free Runtime Verification and Enforcement of Linearizability

  2023cites this paper
• An Efficient Dynamic Analysis Tool for Checking Durable Linearizability

  2021cites this paper
• The Usability Argument for Refinement Typed Genetic Programming

  2020cites this paper
• Refined typed genetic programming as a user interface for genetic programming

  2020cites this paper
• An Analysis of Network-Partitioning Failures in Cloud Systems

  2018cites this paper
• Checking Concurrent Data Structures Under the C/C++11 Memory Model

  2017cites this paper
• Faster Linearizability Checking via P-Compositionality

  2015cites this paper
• Automated and Modular Refinement Reasoning for Concurrent Programs

  2015cites this paper
• CDSSPEC: Testing Concurrent Data Structures Under the C/C++11 Memory Model

  2014influential citation
• Checking Linearizability of Encapsulated Extended Operations

  2014cites this paper
• Assertions for Debugging Parallel Programs

  2013cites this paper
• On the Effectiveness of Contracts as Test Oracles in the Detection and Diagnosis of Faults in Concurrent Object- Oriented Software

  2013cites this paper
• Fully automatic and precise detection of thread safety violations

  2012cites this paper
• Program analyses for automatic and precise error detection

  2012cites this paper
• WSCMon: runtime monitoring of web service orchestration based on refinement checking

  2012cites this paper
• Runtime verification of concurrency-specific correctness criteria

  2011influential citation
• Testing atomicity of composed concurrent operations

  2011cites this paper
• On the Effectiveness of Contracts as Test Oracles in the Detection and Diagnosis of Race Conditions and Deadlocks in Concurrent Object-Oriented Software

  2011cites this paper
• Verification of STM on relaxed memory models

  2011cites this paper
• Testing atomicity of composed concurrent operations

  2011cites this paper
• Parallel assertions for debugging parallel programs

  2011cites this paper
• Location pairs: a test coverage metric for shared-memory concurrent programs

  2011influential citation
• Formalizing and verifying transactional memories

  2010cites this paper
• Verifying linearizability with hindsight

  2010cites this paper
• Automatically Proving Linearizability

  2010cites this paper
• Line-up: a complete and automatic linearizability checker

  2010cites this paper
• Experience with Model Checking Linearizability

  2009cites this paper
• A calculus of atomic actions

  2009cites this paper
• Deriving linearizable fine-grained concurrent objects

  2008cites this paper
• Combining symbolic execution with model checking to verify parallel numerical programs

  2008cites this paper
• Detecting Data Race and Atomicity Violation via Typestate-Guided Static Analysis

  2008cites this paper
• Concurrent Contracts for Java

  2008cites this paper
• Memory model sensitive analysis of concurrent data types

  2007cites this paper
• Temporal Assertions with Parametrised Propositions

  2007cites this paper
• A Causality-Based Runtime Check for (Rollback) Atomicity

  2007cites this paper
• Deterministic replay using processor support and its applications

  2007cites this paper
• Rollback Atomicity

  2007cites this paper
• A Race and Transaction-Aware Runtime for Java

  2007cites this paper
• Automatically classifying benign and harmful data races using replay analysis

  2007cites this paper
• Goldilocks: a race and transaction-aware java runtime

  2007cites this paper
• Vyrd + : A Toolbox for Runtime Verification of Concurrent Software

  2006cites this paper
• Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study

  2006cites this paper
• Integrated Verification for Robust Computing

  2006cites this paper
• VyrdMC: Driving Runtime Refinement Checking with Model Checkers

  2006cites this paper
• A classification of concurrency bugs in java benchmarks by developer intent

  2006cites this paper
• Using model checking with symbolic execution to verify parallel numerical programs

  2006influential citation
• A Novel Test Coverage Metric for Concurrently-Accessed Software Components

  2005influential citation
• Koşutzamanlı Yazılım Bileşenleri için Bir Otomatik Doğrulama Çerçevesi: VyrdMC

  2005influential citation
• about the Internet and Networking : 2010 – 2019

  2003cites this paper