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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic

Cited In (12)

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

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)