On verifying that a concurrent program satisfies a nondeterministic specification
From MaRDI portal
Publication:1123589
DOI10.1016/0020-0190(89)90063-XzbMath0677.68011OpenAlexW2124788813MaRDI QIDQ1123589
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
concurrent programcomplete proof system\(\Pi ^ 1_ 2\)-completenondeterministic \(\omega\)- automaton
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
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