Automatic generation of polynomial loop invariants: algebraic foundations

Consultar RECERCAT

Para acceder a los documentos con el texto completo, por favor, siga el siguiente enlace: http://hdl.handle.net/2117/96839

Título:	Automatic generation of polynomial loop invariants: algebraic foundations
Autor/a:	Rodríguez Carbonell, Enric; Kapur, Dikkar
Otros autores:	Universitat Politècnica de Catalunya. Departament de Ciències de la Computació
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.
Materia(s):	-Àrees temàtiques de la UPC::Informàtica::Programació -Loop invariants -Imperative programs -Maple
Derechos:
Tipo de documento:	Artículo - Versión publicada Informe
Compartir:

Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric

Rodríguez Carbonell, Enric; Oliva, M.; Saltor Soler, Félix Enrique; Campderrich, B.

Bagnara, Roberto; Rodríguez Carbonell, Enric; Zaffanella, Enea

Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto

Bofill Arasa, Miquel; Nieuwenhuis, Robert; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio, Albert

Coordinación

Patrocinio