scientific article; zbMATH DE number 1552508
From MaRDI portal
Publication:4524764
zbMath0970.68149MaRDI QIDQ4524764
Kurt Stenzel, Gerhard Schellhorn, Michael Balser, Wolfgang Reif
Publication date: 15 January 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (20)
Model Checking Simulation Rules for Linearizability ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Automated flaw detection in algebraic specifications ⋮ A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ \( \mathbb{K}\) and KIV: towards deductive verification for arbitrary programming languages ⋮ Completeness of ASM Refinement ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Compositional reasoning using intervals and time reversal ⋮ Proving linearizability with temporal logic ⋮ Completeness of fair ASM refinement ⋮ Verification of Concurrent Systems with VerCors ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Atomic actions, and their refinements to isolated protocols ⋮ Verifying Opacity of a Transactional Mutex Lock ⋮ A Framework for Correctness Criteria on Weak Memory Models ⋮ Relational concurrent refinement. II: Internal operations and outputs ⋮ KIV ⋮ Formal Verification of a Lock-Free Stack with Hazard Pointers ⋮ Cogent: uniqueness types and certifying compilation
Uses Software
This page was built for publication:
