Automating coinduction with case analysis

Eugen Ioan Goriac, Dorel Lucanu, Grigore Roşu

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

Abstract

Coinduction is a major technique employed to prove behavioral properties of systems, such as behavioral equivalence. Its automation is highly desirable, despite the fact that most behavioral problems are -complete. Circular coinduction, which is at the core of the CIRC prover, automates coinduction by systematically deriving new goals and proving existing ones until, hopefully, all goals are proved. Motivated by practical examples, circular coinduction and CIRC have been recently extended with several features, such as special contexts, generalization and simplification. Unfortunately, none of these extensions eliminates the need for case analysis and, consequently, there are still many natural behavioral properties that CIRC cannot prove automatically. This paper presents an extension of circular coinduction with case analysis constructs and reasoning, as well as its implementation in CIRC. To uniformly prove the soundness of this extension, as well as of past and future extensions of circular coinduction and CIRC, this paper also proposes a general correct-extension technique based on equational interpolants.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Proceedings
Pages220-236
Number of pages17
DOIs
StatePublished - 2010
Event12th International Conference on Formal Engineering Methods, ICFEM 2010 - Shanghai, China
Duration: Nov 17 2010Nov 19 2010

Publication series

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

Other

Other12th International Conference on Formal Engineering Methods, ICFEM 2010
CountryChina
CityShanghai
Period11/17/1011/19/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Automating coinduction with case analysis'. Together they form a unique fingerprint.

Cite this