Loading...
Please wait, while we are loading the content...
Similar Documents
Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation
| Content Provider | Hyper Articles en Ligne (HAL) |
|---|---|
| Author | Genet, Thomas Viet Triem Tong, Valérie |
| Abstract | In this paper we present a method to prove automatically initial negative properties on equational specifications. This method tends to combine induction and abstract interpretation. Induction is performed in a classical way using cover sets and rewriting. Abstract interpretation is done using an additional set of equations used to approximate the initial model into an abstract one. Like in the methods dedicated to the proof by induction of positive properties, the equational specification is supposed to be oriented into a terminating, confluent and complete term rewriting system. |
| Related Links | https://inria.hal.science/inria-00072012/file/RR-4576.pdf |
| Language | English |
| Publisher | HAL CCSD |
| Publisher Date | 2002-01-01 |
| Access Restriction | Open |
| Subject Keyword | EQUATIONAL THEORIES ABSTRACT INTERPRETATION REWRITING PROOF BY INDUCTION |
| Content Type | Text |
| Resource Type | Report |
| Subject | Computer Science |