Eugen-Ioan Goriac, Dorel Lucanu, Grigore Rosu

Coinduction is a major technique employed to prove behavioralproperties of systems, such as behavioral equivalence. Its automationis highly desirable, despite the fact that most behavioral problemsare $\Pi_2^0$-complete. Circular coinduction, which is at the core of the CIRCprover, automates coinduction by systematically deriving new goals andproving existing ones until, hopefully, all goals are proved. Motivatedby practical examples, circular coinduction and CIRC have been recentlyextended with several features, such as special contexts, generalizationand simplification. Unfortunately, none of these extensions eliminatesthe need for case analysis and, consequently, there are still many naturalbehavioral properties that CIRC cannot prove automatically. Thispaper presents an extension of circular coinduction with case analysisconstructs and reasoning, as well as its implementation in CIRC. To uniformlyprove the soundness of this extension, as well as of past and futureextensions of circular coinduction and CIRC, this paper also proposes ageneral correct-extension technique based on equational interpolants.

Full Document (PDF)

Bibtex

@TechReport{phd_thesis,
    author = "Eugen-Ioan Goriac and Dorel Lucanu and Grigore Ro{c s}u",
    title = "{Automating Coinduction with Case Analysis}",
    institution = "``Al.I.Cuza'' University of Ia{c s}i, Faculty of Computer Science",
    year = "2010",
    number = "TR 10-05",
    url = "https://publications.info.uaic.ro/technical-reports/archive/tr10-05-2010-automating-coinduction-with-case-analysis/"
}