Verifying temporal properties without temporal logic

DOI10.1145/59287.62028MaRDI QIDQ3832037zbMATH OpenOpenAlexFDO

Authors Bowen Alpern, Fred B. Schneider

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

Büchi automataconcurrent programsprogram verificationreasoning about programs

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)

Recommendations

• scientific article; zbMATH DE number 4153903
• scientific article; zbMATH DE number 3985193
• scientific article; zbMATH DE number 148938
• scientific article; zbMATH DE number 3932379
• Verification of temporal properties

Cited in

(23)

• Proving entailment between conceptual state specifications
• Recognizing safety and liveness
• On verifying that a concurrent program satisfies a nondeterministic specification
• Completing the temporal picture
• Proving correctness with respect to nondeterministic safety specifications
• Interpreting message flow graphs
• Verification of concurrent programs: The automata-theoretic framework
• Provably correct runtime monitoring
• Temporal property verification as a program analysis task
• scientific article; zbMATH DE number 1696765 (Why is no real title available?)
• scientific article; zbMATH DE number 4153903 (Why is no real title available?)
• Verification of temporal properties of nondeterministic algorithms
• Complementary Criteria for Testing Temporal Logic Properties
• Speeding up model checking of timed-models by combining scenario specialization and live component analysis
• scientific article; zbMATH DE number 3898203 (Why is no real title available?)
• scientific article; zbMATH DE number 177500 (Why is no real title available?)
• Verification of temporal properties
• Liminf progress measures
• Verifying properties of HMS machine specifications of real-time systems
• An automata theoretic approach to Temporal Logic
• Hierarchical verification using verification diagrams
• On the refinement of liveness properties of distributed systems
• Combining symmetry reduction and under-approximation for symbolic model checking

This page was built for publication: Verifying temporal properties without temporal logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3832037)