Specifying Concurrent Program Modules

DOI10.1145/69624.357207MaRDI QIDQ3664404zbMATH OpenOpenAlexFDO

Authors 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

zbMATH Keywords

communication protocolsmultiprocessingsemanticsspecificationstemporal assertionstemporal logic

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Theory of operating systems (68N25)

Cited in

(44)

• Proving entailment between conceptual state specifications
• On verifying that a concurrent program satisfies a nondeterministic specification
• Programming in metric temporal logic
• Proving correctness with respect to nondeterministic safety specifications
• Temporal theories as modularisation units for concurrent system specification
• Using mappings to prove timing properties
• Eliminating disjunctions of leads-to properties
• Program composition via unification
• A temporal logic-based approach for the description of object behavior evolution
• Specification of abstract dynamic-data types: A temporal logic approach
• Order-sorted model theory for temporal executable specifications
• Verification of reactive systems using temporal logic with clocks
• Time and logic: A calculus of binary events
• Public data structures: counters as a special case.
• Semantics of temporal classes
• Compositionality in dataflow synchronous languages: Specification and distributed code generation
• Fair simulation
• An optimistic approach to lock-free FIFO queues
• Semantic specification and verification of data flow diagrams
• Capacitated automata and systems
• Stutter-invariant temporal properties are expressible without the next-time operator
• Testing Systems of Concurrent Black-Boxes—An Automata-Theoretic and Decompositional Approach
• Quantitative analysis under fairness constraints
• Control problems in a temporal logic framework
• Search strategies for resolution in temporal logics
• 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
• Modular verification of multithreaded programs
• Temporal logic programming
• Fair simulation
• Automatic temporal verification of buffer systems
• Modal and temporal logics for processes
• On using temporal logic for refinement and compositional verification of concurrent systems
• A logical view of composition
• Compositional transformational design for concurrent programs
• Modular model checking
• Compositionality in dataflow synchronous languages: specification \& code generation
• Encapsulating deontic and branching time specifications
• The existence of refinement mappings
• A\(^ 2\)CCS: Atomic actions for CCS
• 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

This page was built for publication: Specifying Concurrent Program Modules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3664404)