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

Proof by induction
Counterexample
Authentication
State Space
Mathematical Induction
Network protocols
Authentication Protocol
Invariant
Transition Systems
Lemma
Verify
Demonstrate

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.

Induction-guided falsification. / Ogata, Kazuhiro; Nakano, Masahiro; Kong, Weiqiang; Futatsugi, Kokichi.

Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings. Springer Verlag, 2006. p. 114-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4260 LNCS).

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

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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4260 LNCS, Springer Verlag, pp. 114-131, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, 11/1/06.
Ogata K, Nakano M, Kong W, Futatsugi K. Induction-guided falsification. In Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings. Springer Verlag. 2006. p. 114-131. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Ogata, Kazuhiro ; Nakano, Masahiro ; Kong, Weiqiang ; Futatsugi, Kokichi. / Induction-guided falsification. Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings. Springer Verlag, 2006. pp. 114-131 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{27f7d4c2fcbc4d92a3a2684fa8fbe12e,
title = "Induction-guided falsification",
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.",
author = "Kazuhiro Ogata and Masahiro Nakano and Weiqiang Kong and Kokichi Futatsugi",
year = "2006",
month = "1",
day = "1",
language = "English",
isbn = "3540474609",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "114--131",
booktitle = "Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Induction-guided falsification

AU - Ogata, Kazuhiro

AU - Nakano, Masahiro

AU - Kong, Weiqiang

AU - Futatsugi, Kokichi

PY - 2006/1/1

Y1 - 2006/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=33845248661&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33845248661&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540474609

SN - 9783540474609

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 114

EP - 131

BT - Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings

PB - Springer Verlag

ER -