A predicate transformer for progress
From MaRDI portal
Publication:909441
DOI10.1016/0020-0190(90)90218-MzbMath0694.68016OpenAlexW2005989073MaRDI QIDQ909441
Publication date: 1990
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(90)90218-m
Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)
Related Items
Special \(K\)-types, tempered characters and the Beilinson-Bernstein realization, A predicate transformer for the progress property `to-always', A foundation for modular reasoning about safety and progress properties of state-based concurrent programs, A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic, An experiment with the use of predicate transformers in UNITY, On the logic of UNITY, Eliminating the substitution axiom from UNITY logic, Composing leads-to properties
Cites Work
