Proving nondeterministically specified safety properties using progress measures

DOI10.1006/INCO.1993.1064MaRDI QIDQ1317438zbMATH OpenOpenAlexFDO

Authors Nils Klarlund, Fred B. Schneider

Publication date 24 March 1994

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://hdl.handle.net/1813/7044

zbMATH Keywords

nondeterministic automataprogram automatonprogress measuresspecification automatonsubset constructionverification

Mathematics Subject Classification ID

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

Recommendations

• Proving correctness with respect to nondeterministic safety specifications
• Proving Safety Properties of Rewrite Theories
• Proving safety with trace automata and bounded model checking
• Reasoning about safety and liveness properties for probabilistic processes
• Bounded and Unbounded Safety Verification Using Bisimulation Metrics

Cited in

(5)

• On verifying that a concurrent program satisfies a nondeterministic specification
• Proving correctness with respect to nondeterministic safety specifications
• Reversibility in the higher-order \(\pi\)-calculus
• Layout randomization and nondeterminism
• Layout Randomization and Nondeterminism

This page was built for publication: Proving nondeterministically specified safety properties using progress measures

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