Verifying concurrent processes using temporal logic

MaRDI QIDQ1159976zbMATH OpenFDO

Authors Brent T. Hailpern

Publication date 1982

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

zbMATH Keywords

verification of parallel programs

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Cited in

(11)

• Exposure to deadlock for communicating processes is hard to detect
• Removing irrelevant information in temporal resolution proofs
• The sliding-window protocol revisited
• Expressibility of output equals input. Negative and positive results
• Specification and verification of database dynamics
• Control problems in a temporal logic framework
• \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments
• Search strategies for resolution in temporal logics
• Towards a foundation for semantics in complete metric spaces
• A generalized nexttime operator in temporal logic
• Automated temporal reasoning about reactive systems

This page was built for publication: Verifying concurrent processes using temporal logic

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