DSpace Home >
→
Organismes déposants >
→
LIP - Laboratoire de l'Informatique du Parallélisme >
→
View Item >

dc.contributor.author	Laboratoire de l'informatique du parallélisme	en_US
dc.contributor.author	Mounier, V.	en_US
dc.contributor.author	Utard, Gil	en_US
dc.date.accessioned	2007-05-24T11:53:07Z
dc.date.available	2007-05-24T11:53:07Z
dc.date.issued	1993
dc.identifier.other	LIP-RR - 1993-08	en_US
dc.identifier.uri	http://hdl.handle.net/2332/1181
dc.description.abstract	(eng) We give a Hoare-like proof system for the data-parallel language L, and we present an automatic tool to aid program correctness proof. After recalling L's operational semantics, we define an axiomatic semantics. We illustrate proof of L programs with two examples. Then we extend our semantics to weakest precondition, and we deduce techniques for mechanizing program verification from Gordon's verification condition method. We prove its correctness, and we present an implementation of this method in the CENTAUR system.	en_US
dc.format.extent	2+48p	en_US
dc.format.extent	469570 bytes
dc.format.extent	23 bytes
dc.format.mimetype	application/pdf
dc.format.mimetype	application/octet-stream
dc.language.iso	eng	en_US
dc.rights	http://lara.inist.fr/utilisation.jsp	en_US
dc.source.uri	ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR1993/RR1993-08.ps.Z	en_US
dc.subject	Data-Parallel Languages	en_US
dc.subject	Axiomatic Semantics	en
dc.subject	Weakest Precondition	en
dc.subject	Program Verification	en
dc.subject	Program Verification Tools	en
dc.subject	CENTAUR	en
dc.title	Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification	en_US
dc.type	Research report	en_US