On verifying that a concurrent program satisfies a nondeterministic specification
From MaRDI portal
Publication:1123589
DOI10.1016/0020-0190(89)90063-XzbMath0677.68011MaRDI QIDQ1123589
Publication date: 1989
Published in: Information Processing Letters (Search for Journal in Brave)
concurrent program; complete proof system; \(\Pi ^ 1_ 2\)-complete; nondeterministic \(\omega\)- automaton
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
68N01: General topics in the theory of software
68N25: Theory of operating systems
Related Items
Verification by augmented abstraction: The automata-theoretic view, On the refinement of liveness properties of distributed systems, 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, Highly Undecidable Problems For Infinite Computations
Cites Work