- Authors:
- E. A Emerson,
- Chin L Lei
No abstract available.
Cited By
- Reniers M and Willemse T Folk theorems on the correspondence between state-based and event-based systems Proceedings of the 37th international conference on Current trends in theory and practice of computer science, (494-505)
Lichtenstein O and Pnueli A Checking that finite state concurrent programs satisfy their linear specification Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, (97-107)
Recommendations
LTL generalized model checking revisited
Given a 3-valued abstraction of a program (possibly generated using static program analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that ...
Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics
LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer ScienceThree-valued models, in which properties of a system are either true, false or unknown, have recently been advocated as a better representation for reactive program abstractions generated by automatic techniques such as predicate abstraction. Indeed, ...
LTL Generalized Model Checking Revisited
VMCAI '09: Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract InterpretationGiven a 3-valued abstraction of a program (possibly generated using static program analysis and predicate abstraction) and a temporal logic formula, generalized model checking (GMC) checks whether there exists a concretization of that abstraction that ...