Specifying Concurrent Program Modules

From MaRDI portal
Publication:3664404

DOI10.1145/69624.357207zbMath0516.68010OpenAlexW2086070079MaRDI QIDQ3664404

Leslie Lamport

Publication date: 1983

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/69624.357207



Related Items

Program composition via unification, Stutter-invariant temporal properties are expressible without the next-time operator, Proving entailment between conceptual state specifications, A temporal logic-based approach for the description of object behavior evolution, Control problems in a temporal logic framework, On verifying that a concurrent program satisfies a nondeterministic specification, Programming in metric temporal logic, Specification of abstract dynamic-data types: A temporal logic approach, Order-sorted model theory for temporal executable specifications, A\(^ 2\)CCS: Atomic actions for CCS, An optimistic approach to lock-free FIFO queues, Verifying atomic data types, Algebraic specification of concurrent systems, Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems, Design and analysis of dynamic leader election protocols in broadcast networks, Action systems in incremental and aspect-oriented modeling, Safety assurance via on-line monitoring, Proving correctness with respect to nondeterministic safety specifications, On using temporal logic for refinement and compositional verification of concurrent systems, Temporal theories as modularisation units for concurrent system specification, Search strategies for resolution in temporal logics, A logical view of composition, Using mappings to prove timing properties, Fair simulation, Modular verification of multithreaded programs, Encapsulating deontic and branching time specifications, Temporal logic programming, Semantic specification and verification of data flow diagrams, Capacitated automata and systems, Time and logic: A calculus of binary events, Quantitative Analysis under Fairness Constraints, Verification of reactive systems using temporal logic with clocks, Public data structures: counters as a special case., Semantics of temporal classes, Compositionality in dataflow synchronous languages: Specification and distributed code generation, Fair simulation, Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach, The existence of refinement mappings, Eliminating disjunctions of leads-to properties