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

verificationsubset constructionnondeterministic automataprogram automatonprogress measuresspecification automaton

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) 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
• scientific article; zbMATH DE number 1318512
• Bounded and Unbounded Safety Verification Using Bisimulation Metrics

Cited in

(4)

• Layout Randomization and Nondeterminism
• On verifying that a concurrent program satisfies a nondeterministic specification
• Reversibility in the higher-order \(\pi\)-calculus
• 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)