Induction-guided falsification

Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi

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

    15 Citations (Scopus)


    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
    Number of pages18
    ISBN (Print)3540474609, 9783540474609
    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


    Other8th International Conference on Formal Engineering Methods, ICFEM 2006

    All Science Journal Classification (ASJC) codes

    • Theoretical Computer Science
    • Computer Science(all)


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

    Cite this