Axiomatic Semantics of Data-Parallel Languages; Automatization of Programs Verification

DSpace/Manakin Repository

Show simple item record

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

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search DSpace

Advanced Search


My Account

Bookmark and Share