Verification of sequential and concurrent programs
From MaRDI portal
Publication:837527
DOI10.1007/978-1-84882-745-5zbMath1183.68361OpenAlexW2569787747MaRDI QIDQ837527
Frank S. de Boer, Krzysztof R. Apt, Ernst-Ruediger Olderog
Publication date: 10 September 2009
Published in: Texts in Computer Science (Search for Journal in Brave)
Full work available at URL: https://ir.cwi.nl/pub/14569
Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items (42)
A Hoare Logic for GPU Kernels ⋮ Indexed and fibered structures for partial and total correctness assertions ⋮ A UTP approach for rTiMo ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Being and Change: Reasoning About Invariance ⋮ Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos ⋮ Introduction to Model Checking ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Certified verification of relational properties ⋮ A Hoare Logic for SIMT Programs ⋮ Tournaments for mutual exclusion: verification and concurrent complexity ⋮ Proving correctness of imperative programs by linearizing constrained Horn clauses ⋮ Proof systems for planning under 0-approximation semantics ⋮ Semantic embedding for quantum algorithms ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ A dynamic logic with branching modalities ⋮ Denotational and algebraic semantics for the CaIT calculus ⋮ Experiments in program verification using Event-B ⋮ UTP Semantics for rTiMo ⋮ Verification of object-oriented programs: a transformational approach ⋮ Unnamed Item ⋮ Reasoning about actions with loops via Hoare logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Starvation-free mutual exclusion with semaphores ⋮ Proving Quicksort Correct in Event-B ⋮ A proof system for adaptable class hierarchies ⋮ Toward automatic verification of quantum programs ⋮ Verification of concurrent programs using Petri net unfoldings ⋮ Symbolic execution formally explained ⋮ Using Hoare Logic in a Process Algebra Setting ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Incremental reasoning with lazy behavioral subtyping for multiple inheritance ⋮ Algebras for iteration and infinite computations ⋮ Fifty years of Hoare's logic ⋮ Building program construction and verification tools from algebraic principles ⋮ Correctness and concurrent complexity of the black-white bakery algorithm ⋮ Verifying traits: an incremental proof system for fine-grained reuse ⋮ A proof system for disjoint parallel quantum programs ⋮ Monadic second-order incorrectness logic for GP 2 ⋮ Proof pearl: The KeY to correct and stable sorting ⋮ Incorrectness logic for graph programs
Uses Software
This page was built for publication: Verification of sequential and concurrent programs
