Automatic generation of polynomial loop invariants: algebraic foundations
Visualitza/Obre
Estadístiques de LA Referencia / Recolecta
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/96839
Tipus de documentReport de recerca
Data publicació2004-01
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
A general framework is presented for automating the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it is shown how this abstract approach can be used to automatically infer polynomial invariants. The method has been implemented in Maple. Evidence of its practical interest is shown by means of several non-trivial examples, for which the polynomial loop invariants generated are directly applicable for proving correctness by means of a simple verifier.
CitacióRodriguez, E., Kapur, D. "Automatic generation of polynomial loop invariants: algebraic foundations". 2004.
Forma partLSI-04-1-R
Col·leccions
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
R04-1.ps | 476,5Kb | Postscript | Visualitza/Obre |