Circular coinduction with special contexts

Dorel Lucanu, Grigore Roşu

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

Abstract

Coinductive proofs of behavioral equivalence often require human ingenuity, in that one is expected to provide a "good" relation extending one's goal with additional lemmas, making automation of coinduction a challenging problem. Since behavioral satisfaction is a Π02 -hard problem, one can only expect techniques and methods that approximate the behavioral equivalence. Circular coinduction is an automated technique to prove behavioral equivalence by systematically exploring the behaviors of the property to prove: if all behaviors are circular then the property holds. Empirical evidence shows that one of the major reasons for which circular coinduction does not terminate in practice is that the circular behaviors may be guarded by a context. However, not all contexts are safe. This paper proposes a large class of contexts which are safe guards for circular behaviors, called special contexts, and extends circular coinduction appropriately. The resulting technique has been implemented in the CIRC prover and experiments show that the new technique can prove many interesting behavioral properties fully automatically.

Original languageEnglish (US)
Title of host publicationFormal Methods and Software Engineering - 11th International Conference on Formal Engineering Methods, ICFEM 2009, Proceedings
Pages639-659
Number of pages21
DOIs
StatePublished - 2009
Event11th International Conference on Formal Engineering Methods, ICFEM 2009 - Rio de Janeiro, Brazil
Duration: Dec 9 2009Dec 12 2009

Publication series

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

Other

Other11th International Conference on Formal Engineering Methods, ICFEM 2009
CountryBrazil
CityRio de Janeiro
Period12/9/0912/12/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Circular coinduction with special contexts'. Together they form a unique fingerprint.

Cite this