Verifying atomic data types

DOI10.1007/BF01379184zbMath0701.68076OpenAlexW2013433898MaRDI QIDQ914403

Jeannette M. Wing

Publication date: 1989

Published in: International Journal of Parallel Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01379184

zbMATH Keywords

distributed systemsfault-toleranceprogram verificationabstract data typesAtomic transactions

Mathematics Subject Classification ID

Network design and communication in computer systems (68M10) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Reliability, testing and fault tolerance of networks and computer systems (68M15)

Uses Software

• LARCH

Cites Work

• Unnamed Item
• Unnamed Item
• Adequate proof principles for invariance and liveness properties of concurrent programs
• The existence of refinement mappings
• Introduction to the theory of nested transactions
• A formal model of atomicity in asynchronous systems
• Proof of correctness of data representations
• Guardians and Actions: Linguistic Support for Robust, Distributed Programs
• Specifying Concurrent Program Modules
• The serializability of concurrent database updates
• A Proof System for Communicating Sequential Processes
• Verifying properties of parallel programs
• The notions of consistency and predicate locks in a database system
• Time, clocks, and the ordering of events in a distributed system
• On the correctness of orphan management algorithms

This page was built for publication: Verifying atomic data types