Concurrency verification. Introduction to compositional and noncompositional methods
temporal logicHoare logicprogram verificationsoundnessconcurrent programcompositional reasoningprogram transformationtransition systemsemantic completenessshared variableinductive assertionabsence of deadlockassumption commitmentcommunication-closed-layers paradigmnoncompositional proof methodrely-guarantee methodsynchronous message
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
- Verifying correctness of persistent concurrent data structures: a sound and complete method
- Encoding fairness in a synchronous concurrent program algebra
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- A unified approach of program verification
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Compositional Bitvector Analysis for Concurrent Programs with Nested Locks
- Synchronous message passing: on the relation between bisimulation and refusal equivalence
- Meanings of model checking
- Compositional verification of sequential programs with procedures
- Splitting atoms safely
- Formal sequentialization of distributed systems via program rewriting
- Compositional Nonblocking Verification Using Generalized Nonblocking Abstractions
- Proving linearizability with temporal logic
- Extending rely-guarantee thinking to handle real-time scheduling
- (Co)inductive proof systems for compositional proofs in reachability logic
- Automated compositional proofs for real-time systems
- Balancing expressiveness in formal approaches to concurrency
- Splitting Atoms with Rely/Guarantee Conditions Coupled with Data Reification
- Convolution and concurrency
- A coinductive calculus for asynchronous side-effecting processes
- Mechanizing a process algebra for network protocols
- Elucidating concurrent algorithms via layers of abstraction and reification
- Fifty years of Hoare's logic
- Formal verification of a lock-free stack with hazard pointers
- AUTOMATED COMPOSITIONAL REASONING OF INTUITIONISTICALLY CLOSED REGULAR PROPERTIES
- Towards a thread-local proof technique for starvation freedom
- Automated Compositional Reasoning of Intuitionistically Closed Regular Properties
- Semantic models of a timed distributed dataspace architecture
- Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
- Compositional reasoning using intervals and time reversal
- An operational semantics for object-oriented concepts based on the class hierarchy
- Derivation of concurrent programs by stepwise scheduling of Event-B models
- A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
- On rely-guarantee reasoning
- Compositional reasoning about active objects with shared futures
- Just testing
- Static analysis of run-time errors in embedded critical parallel C programs
- Formal communication elimination and sequentialization equivalence proofs for distributed system models
- Generalised rely-guarantee concurrency: an algebraic foundation
- Fine-grained concurrency with separation logic
- Compositional CSP traces refinement checking
- Contracts for BIP: Hierarchical Interaction Models for Compositional Verification
- A framework for compositional verification of security protocols
- Proving reachability-logic formulas incrementally
- Local proofs for global safety properties
- Assumption-commitment support for CSP model checking
- A system for compositional verification of asynchronous objects
- Designing a semantic model for a wide-spectrum language with concurrency
- Assumption-commitment support for CSP model checking
- Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
- Compositional reasoning for shared-variable concurrent programs
- A Bibliography of Willem-Paul de Roever
- An application of temporal projection to interleaving concurrency
- Verifying distributed systems: the operational approach
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos
- A verification-driven framework for iterative design of controllers
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts
- Local symmetry and compositional verification
- Towards a hybrid dynamic logic for hybrid dynamic systems
- scientific article; zbMATH DE number 1476492 (Why is no real title available?)
- A survey of verification techniques for parallel programs
- Axiomatic characterization of trace reachability for concurrent objects
- Practical abstractions for automated verification of message passing concurrency
- The symbiosis of concurrency and verification: teaching and case studies
- Compositional reasoning
- scientific article; zbMATH DE number 3956417 (Why is no real title available?)
This page was built for publication: Concurrency verification. Introduction to compositional and noncompositional methods
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2768503)
