Induction-guided falsification

Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    15 Citations (Scopus)

    Abstract

    The induction-guided falsification searches a bounded reachable state space of a transition system for a counterexample that the system satisfies an invariant property. If no counterexamples are found, it tries to verify that the system satisfies the property by mathematical induction on the structure of the reachable state space of the system, from which some other invariant properties may be obtained as lemmas. The verification and falsification process is repeated for each of the properties until a counterexample is found or the verification is completed. The NSPK authentication protocol is used as an example to demonstrate the induction-guided falsification.

    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings
    PublisherSpringer Verlag
    Pages114-131
    Number of pages18
    ISBN (Print)3540474609, 9783540474609
    DOIs
    Publication statusPublished - 2006
    Event8th International Conference on Formal Engineering Methods, ICFEM 2006 - Macao, China
    Duration: Nov 1 2006Nov 3 2006

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    Volume4260 LNCS
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Other

    Other8th International Conference on Formal Engineering Methods, ICFEM 2006
    CountryChina
    CityMacao
    Period11/1/0611/3/06

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)

    Fingerprint Dive into the research topics of 'Induction-guided falsification'. Together they form a unique fingerprint.

    Cite this