@inproceedings{9d0f971eb1c4412a9b78ac4b22b88e78,
title = "Real-time system verification techniques based on abstraction/deduction and model checking",
abstract = "Abstract. Our research focuses on verification techniques for real-time systems based on predicate abstractions. These techniques aim to combine abstract interpretation, model checking, and theorem proving in order to obtain a powerful and highly automatic verification environment for real-time systems. One drawback of current real-time model checking approaches is the limited size of the systems that can be analyzed. For the computation of finite abstractions in the way of infinite-state systems analysis, we propose an Iterative-Abstract-Refinement algorithm. Using our algorithm, we can reduce the aforementioned drawbacks associated with the application of real-time model checking such as the limited applicability due to state space explosion characteristics",
keywords = "conference contrib. refereed, Conf.proc. > 3 pag",
author = "EY Kang",
note = "neo; IFM 2005 Doctoral symposium on Integrated Formal Methods, Eindhoven ; Conference date: 29-11-2005 Through 02-12-2005",
year = "2005",
language = "Undefined/Unknown",
publisher = "Eindhoven University of Technology",
pages = "26--32",
editor = "J Romijn and G Smith and {van de Pol}, J",
booktitle = "IFM 2005 Doctoral symposium on Integrated Formal Methods",
}