Induction-guided falsification

Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi

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

14 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
Publication statusPublished - Jan 1 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

    Fingerprint

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Ogata, K., Nakano, M., Kong, W., & Futatsugi, K. (2006). Induction-guided falsification. In Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings (pp. 114-131). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4260 LNCS). Springer Verlag.