Skip to Main content Skip to Navigation
Journal articles

Observational proofs by rewriting

Adel Bouhoula 1 Michaël Rusinowitch 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Observability concepts contribute to a better understanding of software correctness. In order to prove observational properties, the concept of Context Induction has been developed by Hennicker (Hennicker, Formal Aspects of Computing 3(4) (1991) 326–345). We propose in this paper to embed Context Induction in the implicit induction framework of (Bouhoula and Rusinowitch, Journal of Automated Reasoning 14(2) (1995) 189–235). The proof system we obtain applies to conditional specifications. It allows for many rewriting techniques and for the refutation of false observational conjectures. Under reasonable assumptions our method is refutationally complete, i.e. it can refute any conjecture which is not observationally valid. Moreover this proof system is operational: it has been implemented within the Spike prover and interesting computer experiments are reported.
Document type :
Journal articles
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:49:54 PM
Last modification on : Friday, February 4, 2022 - 3:19:24 AM

Links full text




Adel Bouhoula, Michaël Rusinowitch. Observational proofs by rewriting. Theoretical Computer Science, Elsevier, 2002, 275 (1-2), pp.675-698. ⟨10.1016/S0304-3975(01)00333-4⟩. ⟨inria-00100714⟩



Record views