On verifying that a concurrent program satisfies a nondeterministic specification

DOI10.1016/0020-0190(89)90063-XzbMATH Open0677.68011OpenAlexW2124788813MaRDI QIDQ1123589FDOQ1123589

Authors A. P. Sistla

Publication date 1989

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

Full work available at URL https://doi.org/10.1016/0020-0190(89)90063-x

zbMATH Keywords

concurrent programcomplete proof system\(\Pi ^ 1_ 2\)-completenondeterministic \(\omega\)- automaton

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Recommendations

• The complexity of probabilistic verification
• Proving correctness with respect to nondeterministic safety specifications
• Model checking concurrent programs with nondeterminism and randomization
• Proving nondeterministically specified safety properties using progress measures
• scientific article; zbMATH DE number 3936484

Cites work

• scientific article; zbMATH DE number 3972158 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic

Cited in

(12)

• On the refinement of liveness properties of distributed systems
• On the computation of counterexamples in compositional nonblocking verification
• Model checking concurrent programs with nondeterminism and randomization
• Verification by augmented abstraction: The automata-theoretic view
• Verification of concurrent programs: The automata-theoretic framework
• Formal verification of language-based concurrent noninterference
• Proving correctness with respect to nondeterministic safety specifications
• Highly Undecidable Problems For Infinite Computations
• Classes of timed automata and the undecidability of universality
• Distributed Computing
• Conformance Tests as Checking Experiments for Partial Nondeterministic FSM
• Adequate proof principles for invariance and liveness properties of concurrent programs

This page was built for publication: On verifying that a concurrent program satisfies a nondeterministic specification

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