[CAM12] Maximal and Compositional Pattern-Based Loop Invariants

Conférence Internationale avec comité de lecture : Formal method 2012 (FME), August 2012, Vol. 7436, pp.37-51, Series LNCS, Paris, France,

Auteurs: P. Courtieu , M. Aponte , Y. Moy , M. Sango

Mots clés: loop invariant, proof of programs, semantics, Hoare logic

Résumé: We define a framework for automatic generation of loop invariants for a small language. The method proceeds by 1) translation to an intermediate language of parallel guarded assignments 2) pattern detection. The patterns are modular in the sense that they are independent of the loop they appear in. Some maximality results are also proved on some pattern invariants.

Equipe: sys

BibTeX

@inproceedings {
	CAM12,
	title	=	"{Maximal and Compositional Pattern-Based Loop Invariants}",
	author	=	" P. Courtieu and M. Aponte and Y. Moy and M. Sango ",
	booktitle	=	"{Formal method 2012 (FME)}",
	year	=	2012,
	month	=	"August",
	series	=	"LNCS",
	volume	=	7436,
	pages	=	"37-51",
	address	=	"Paris, France",
}