Verifying temporal properties without temporal logic

DOI10.1145/59287.62028zbMath0676.68003OpenAlexW1986033227MaRDI QIDQ3832037

Fred B. Schneider, Bowen Alpern

Publication date: 1989

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: http://www.acm.org/pubs/contents/journals/toplas/1989-11/

zbMATH Keywords

concurrent programsBüchi automatareasoning about programsprogram verification

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)

Related Items

Proving entailment between conceptual state specifications, Recognizing safety and liveness, Interpreting message flow graphs, Provably correct runtime monitoring, On verifying that a concurrent program satisfies a nondeterministic specification, Liminf progress measures, Completing the temporal picture, Proving correctness with respect to nondeterministic safety specifications, Verification of concurrent programs: The automata-theoretic framework, On the refinement of liveness properties of distributed systems, Speeding Up Model Checking of Timed-Models by Combining Scenario Specialization and Live Component Analysis, Combining symmetry reduction and under-approximation for symbolic model checking