Proving correctness with respect to nondeterministic safety specifications

DOI10.1016/0020-0190(91)90061-LzbMath0735.68028OpenAlexW2147133238MaRDI QIDQ1182117

A. P. Sistla

Publication date: 27 June 1992

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(91)90061-l

zbMATH Keywords

concurrencyspecificationscomplete proof systemnondeterministic automata

Mathematics Subject Classification ID

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

Related Items (4)

Proving correctness with respect to nondeterministic safety specifications ⋮ Completeness of ASM Refinement ⋮ Completeness of fair ASM refinement ⋮ On the refinement of liveness properties of distributed systems

Cites Work

• Recognizing safety and liveness
• On verifying that a concurrent program satisfies a nondeterministic specification
• Proving correctness with respect to nondeterministic safety specifications
• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic

This page was built for publication: Proving correctness with respect to nondeterministic safety specifications