{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T12:43:40Z","timestamp":1648817020811},"reference-count":22,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1997,12,1]],"date-time":"1997-12-01T00:00:00Z","timestamp":880934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5707,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1997,12]]},"DOI":"10.1016\/s0304-3975(97)00041-8","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T15:40:02Z","timestamp":1049730002000},"page":"71-107","source":"Crossref","is-referenced-by-count":4,"title":["Formal validation of data-parallel programs: a two-component assertional proof system for a simple language"],"prefix":"10.1016","volume":"189","author":[{"given":"Luc","family":"Boug\u00e9","sequence":"first","affiliation":[]},{"given":"David","family":"Cachera","sequence":"additional","affiliation":[]},{"given":"Yann","family":"Le Guyadec","sequence":"additional","affiliation":[]},{"given":"Gil","family":"Utard","sequence":"additional","affiliation":[]},{"given":"Bernard","family":"Virot","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(97)00041-8_BIB1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4376-0","article-title":"Verification of Sequential and Concurrent Programs","author":"Apt","year":"1991"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB2","series-title":"the Data-Parallel Programming Model","first-page":"4","article-title":"The Data-Parallel Programming Model: A Semantic Perspective","volume":"vol. 1132","author":"Boug\u00e9","year":"1996"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB3","series-title":"Proc. IFIP WG 10.3, Applications in Parallel and Distributed Computing","first-page":"63","article-title":"A proof system for a simple data-parallel programming language","author":"Boug\u00e9","year":"1994"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB4","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1016\/0167-739X(92)90069-N","article-title":"Control structures for data-parallel SIMD languages: semantics and implementation","volume":"8","author":"Boug\u00e9","year":"1992","journal-title":"Future Generation Computer Systems"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB5","article-title":"Escape constructs in data-parallel languages: semantics and proof system","author":"Boug\u00e9","year":"1994"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB6","article-title":"Two completeness results about a proof system for simple data-parallel language","author":"Cachera","year":"1995"},{"issue":"4","key":"10.1016\/S0304-3975(97)00041-8_BIB7","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1142\/S0129626496000455","article-title":"Proving data-parallel programs: a unifying approach","volume":"6","author":"Cachera","year":"1996","journal-title":"Parallel Process. Lett. 1996"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB8","series-title":"3rd Conf. Found. Softw. Techn. and Theor. Comp. Science","article-title":"On the completeness of a proof system for a synchronous parallel programming language","author":"Clint","year":"1983"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB9","series-title":"Data-Parallel C Extension","year":"1994"},{"issue":"2","key":"10.1016\/S0304-3975(97)00041-8_BIB10","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1006\/jpdc.1994.1080","article-title":"An approach to correctness of data-parallel algorithms","volume":"22","author":"Gabarr\u00f3","year":"1994","journal-title":"J. Parallel and Distrib. Comput."},{"key":"10.1016\/S0304-3975(97)00041-8_BIB11","series-title":"Programming Language Theory and its Implementation","author":"Gordon","year":"1988"},{"issue":"12","key":"10.1016\/S0304-3975(97)00041-8_BIB12","doi-asserted-by":"crossref","first-page":"1170","DOI":"10.1145\/7902.7903","article-title":"Data parallel algorithms","volume":"29","author":"Hillis","year":"1986","journal-title":"Comm. ACM"},{"issue":"10","key":"10.1016\/S0304-3975(97)00041-8_BIB13","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Comm. ACM"},{"issue":"3","key":"10.1016\/S0304-3975(97)00041-8_BIB14","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1142\/S012962649600039X","article-title":"Sequential-like proofs of data-parallel programs","volume":"6","author":"Le Guyadec","year":"1996","journal-title":"Parallel Process. Lett. (1996)"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB15","author":"MasPar Computer Corporation, Sunnyvale, CA","year":"1990","journal-title":"Maspar Parallel Application Language Reference Manual"},{"issue":"5","key":"10.1016\/S0304-3975(97)00041-8_BIB16","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1145\/360051.360224","article-title":"Verifying properties of parallel programs: an axiomatic approach","volume":"19","author":"Owicki","year":"1976","journal-title":"Comm. ACM"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB17","article-title":"HyperC specification document","author":"Paris","year":"1993"},{"issue":"2","key":"10.1016\/S0304-3975(97)00041-8_BIB18","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1145\/357073.357075","article-title":"A language for array and vector processors","volume":"1","author":"Perrot","year":"1979","journal-title":"ACM Trans. Progr. Lang."},{"key":"10.1016\/S0304-3975(97)00041-8_BIB19","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1006\/jpdc.1995.1073","article-title":"Reasoning about data-parallel array assignment","volume":"27","author":"Stewart","year":"1985","journal-title":"J. Parallel Distrib. Comput."},{"key":"10.1016\/S0304-3975(97)00041-8_BIB20","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/BF01932133","article-title":"An axiomatic treatment of SIMD assignment","volume":"30","author":"Stewart","year":"1990","journal-title":"BIT"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB21","author":"Thinking Machine Corporation, Cambridge, MA","year":"1990","journal-title":"C\u2217 programming guide"},{"key":"10.1016\/S0304-3975(97)00041-8_BIB22","article-title":"Semantics of data-parallel languages. Applications to validation and compilation","author":"Utard","year":"1995"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597000418?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597000418?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T08:59:46Z","timestamp":1555405186000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397597000418"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,12]]},"references-count":22,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1997,12]]}},"alternative-id":["S0304397597000418"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(97)00041-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1997,12]]}}}