• EY Kang
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
Original languageUndefined/Unknown
Title of host publicationIFM 2005 Doctoral symposium on Integrated Formal Methods
EditorsJ Romijn, G Smith, J van de Pol
Place of PublicationEindhoven
PublisherEindhoven University of Technology
Number of pages7
Publication statusPublished - 2005
EventIFM 2005 Doctoral symposium on Integrated Formal Methods, Eindhoven - Eindhoven
Duration: 29 Nov 20052 Dec 2005

Publication series

PublisherEindhoven University of Technology
NameComputer Science Reports
ISSN (Print)0926-4515


ConferenceIFM 2005 Doctoral symposium on Integrated Formal Methods, Eindhoven

    Research areas

  • conference contrib. refereed, Conf.proc. > 3 pag

ID: 1974198