On verifying that a concurrent program satisfies a nondeterministic specification

DOI10.1016/0020-0190(89)90063-XzbMath0677.68011OpenAlexW2124788813MaRDI QIDQ1123589

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

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

Related Items (max. 100)

Proving correctness with respect to nondeterministic safety specifications ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Highly Undecidable Problems For Infinite Computations ⋮ On the refinement of liveness properties of distributed systems ⋮ Classes of Timed Automata and the Undecidability of Universality

Cites Work

• Specifying Concurrent Program Modules
• Verifying temporal properties without temporal logic
• Unnamed Item
• Unnamed Item

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