Circular Coinduction with Special Contexts

Lucanu, Dorel; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/11525 Copy

Description

Title

Circular Coinduction with Special Contexts

Author(s)

• Lucanu, Dorel
• Rosu, Grigore

Issue Date

2009-02

Keyword(s)

computer science

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 0 2 -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."

Type of Resource

text

Permalink

http://hdl.handle.net/2142/11525

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections