{"id":189370,"date":"2013-05-21T00:00:00","date_gmt":"2013-05-22T15:08:33","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/msr-research-item\/verifying-data-parallel-programs-using-sequential-program-verification-technology\/"},"modified":"2016-08-02T06:11:45","modified_gmt":"2016-08-02T13:11:45","slug":"verifying-data-parallel-programs-using-sequential-program-verification-technology","status":"publish","type":"msr-video","link":"https:\/\/www.microsoft.com\/en-us\/research\/video\/verifying-data-parallel-programs-using-sequential-program-verification-technology\/","title":{"rendered":"Verifying Data Parallel Programs Using Sequential Program Verification Technology"},"content":{"rendered":"<div class=\"asset-content\">\n<p>I will report on recent work in the Multicore Programming Group at Imperial on the verification of data parallel programs. The principal focus of the talk will be on GPUVerify, a verification technique and tool for GPU kernels written in OpenCL and CUDA.  This project started when I was a Visiting Researcher at MSR during 2011, and has evolved into a now fairly usable tool which we are pushing to GPU programmers.  GPUVerify achieves scalability by transforming a massively parallel GPU kernel into a sequential program that can be checked using existing theorem-proving based tools such as Microsoft&#8217;s Boogie.  I will describe how this transformation works, discuss practical issues associated with building a tool chain that can operate directly on OpenCL and CUDA source code, and describe recent developments related to improving the efficiency of invariant inference.  I will then briefly discuss our current thoughts about how the idea of using sequential verification technology to verify data parallel programs might be extended to other programming models, in particular OpenMP.  For an introduction to GPUVerify check out this video: http:\/\/www.youtube.com\/watch?v=l8ysBPV8OvA<\/p>\n<\/div>\n<p><!-- .asset-content --><\/p>\n","protected":false},"excerpt":{"rendered":"<p>I will report on recent work in the Multicore Programming Group at Imperial on the verification of data parallel programs. The principal focus of the talk will be on GPUVerify, a verification technique and tool for GPU kernels written in OpenCL and CUDA. This project started when I was a Visiting Researcher at MSR during [&hellip;]<\/p>\n","protected":false},"featured_media":197622,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[],"msr-video-type":[206954],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-189370","msr-video","type-msr-video","status-publish","has-post-thumbnail","hentry","msr-video-type-microsoft-research-talks","msr-locale-en_us"],"msr_download_urls":"","msr_external_url":"https:\/\/youtu.be\/fDeYPsyWFs\/","msr_secondary_video_url":"","msr_video_file":"","_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189370"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-video"}],"version-history":[{"count":0,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video\/189370\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/197622"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=189370"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=189370"},{"taxonomy":"msr-video-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-video-type?post=189370"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=189370"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=189370"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=189370"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}