| Year | 2009 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Gheorghe Grigoras, Dorel Lucanu, Georgiana Caltais, Eugen Goriac |
Links
Abstract
Behavioral equivalence is indistinguishably under experiments: two elements are behavioral equivalent iff eachexperiment returns the same value for the two elements. Behavioral equivalence can be proved by coinduction. CIRCis a theorem prover which implements circular coinduction,an efficient coinductive technique. Equational attributes refer properties like associativity, commutativity, unity, etc. If these attributes are behaviorally satisfied, then we refer them as behavioral attributes. Two problems regarding these properties are important: expressing the commutativity as a rewrite rule leads to non-termination and their use as attributes requires a careful handling in the proving process. In this paper we present how these attributes are automatically checked in CIRC and we prove that this extension is sound.