scientific article; zbMATH DE number 1390334

MaRDI QIDQ4934623zbMATH OpenFDO

Authors Leslie Lamport

Publication date 6 May 2001

zbMATH Keywords

specification techniquetemporal logic of actionsTLA\(^+\)

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Formal Specification of Concurrent Systems: A Structured Approach
• A formal system for specification analysis of concurrent programs
• scientific article; zbMATH DE number 3898214
• Concurrent specifications beyond linearizability
• A functional programming approach to the specification and verification of concurrent systems
• Specification and verification of concurrent programs through refinements
• Specification and verification of concurrent systems by causality and realizability

Cited in

(26)

• Fast Paxos
• Lower bounds for asynchronous consensus
• A modular framework for verifying versatile distributed systems
• Information flow control in software DB units based on formal verification
• Specifying reversibility with \(\mathrm{TLA}^+\)
• Implementing dataflow with threads
• Domain science and engineering from computer science to the sciences of informatics. I: Engineering
• Automatic verification of TLA\(^{ + }\) proof obligations with SMT solvers
• Byzantizing Paxos by refinement
• On the diversity of asynchronous communication
• The PlusCal Algorithm Language
• A Reduction Theorem for the Verification of Round-Based Distributed Algorithms
• Combinations of Theories for Decidable Fragments of First-Order Logic
• scientific article; zbMATH DE number 2064460 (Why is no real title available?)
• scientific article; zbMATH DE number 1487859 (Why is no real title available?)
• Domain science and engineering from computer science to the sciences of informatics. II: Science
• scientific article; zbMATH DE number 2172804 (Why is no real title available?)
• scientific article; zbMATH DE number 1390253 (Why is no real title available?)
• scientific article; zbMATH DE number 1405446 (Why is no real title available?)
• Manifest domains: analysis and description
• Extracting Symbolic Transitions from TLA$$^{+}$$+ Specifications
• Tasks in modular proofs of concurrent algorithms
• Domain modelling: a foundation for software development
• ConcurrentHOL
• Improving automation for higher-order proof steps
• Deductive verification of alternating systems

Describes a project that uses

Uses Software

• TLAPS

This page was built for publication:

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