### 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 language | English |
---|---|

Title of host publication | Formal Methods and Software Engineering - 8th International Conference on Formal Engineering Methods, ICFEM 2006, Proceedings |

Publisher | Springer Verlag |

Pages | 114-131 |

Number of pages | 18 |

ISBN (Print) | 3540474609, 9783540474609 |

Publication status | Published - Jan 1 2006 |

Event | 8th International Conference on Formal Engineering Methods, ICFEM 2006 - Macao, China Duration: Nov 1 2006 → Nov 3 2006 |

### Publication series

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

Volume | 4260 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Other

Other | 8th International Conference on Formal Engineering Methods, ICFEM 2006 |
---|---|

Country | China |

City | Macao |

Period | 11/1/06 → 11/3/06 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### Cite this

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

}

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 -