Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation

Thomas Genet 1 Valérie Viet Triem Tong 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072012
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:33:47 PM
Last modification on : Thursday, December 13, 2018 - 8:06:02 PM
Long-term archiving on : Sunday, April 4, 2010 - 10:48:50 PM

Identifiers

  • HAL Id : inria-00072012, version 1

Citation

Thomas Genet, Valérie Viet Triem Tong. Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation. [Research Report] RR-4576, INRIA. 2002. ⟨inria-00072012⟩

Share

Metrics

Record views

362

Files downloads

99