{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:56Z","timestamp":1784233016693,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,11,7]],"date-time":"2010-11-07T00:00:00Z","timestamp":1289088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,11,7]]},"DOI":"10.1145\/1882362.1882392","type":"proceedings-article","created":{"date-parts":[[2010,11,12]],"date-time":"2010-11-12T14:38:38Z","timestamp":1289572718000},"page":"137-142","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Top ten ways to make formal methods for HPC practical"],"prefix":"10.1145","author":[{"given":"Ganesh L.","family":"Gopalakrishnan","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,11,7]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"MPI 2.1 Standard. MPI Standard 2.1. http:\/\/www.mpi-forum.org\/docs\/.  MPI 2.1 Standard. MPI Standard 2.1. http:\/\/www.mpi-forum.org\/docs\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763053"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.v40:1"},{"key":"e_1_3_2_1_5_1","unstructured":"OpenCL: http:\/\/www.khronos.org\/opencl.  OpenCL: http:\/\/www.khronos.org\/opencl."},{"key":"e_1_3_2_1_6_1","volume-title":"Programming Massively Parallel Processors. Morgan Kauffman","author":"David","year":"2010","unstructured":"David B. Kirk and Wen-mei W. Hwu , Programming Massively Parallel Processors. Morgan Kauffman , 2010 . David B. Kirk and Wen-mei W. Hwu, Programming Massively Parallel Processors. Morgan Kauffman, 2010."},{"key":"e_1_3_2_1_7_1","volume-title":"Available Online via ScienceDirect","author":"Li Guodong","year":"2010","unstructured":"Guodong Li , Robert Palmer , Michael DeLisi , Ganesh Gopalakrishnan , and Robert M. Kirby . Formal specification of MPI 2.0. Science of Computer Programming , Accepted. Available Online via ScienceDirect , June 15, 2010 . http:\/\/www.sd.ddns.info\/ Guodong Li, Robert Palmer, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby. Formal specification of MPI 2.0. Science of Computer Programming, Accepted. Available Online via ScienceDirect, June 15, 2010. http:\/\/www.sd.ddns.info\/"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504214"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351145"},{"key":"e_1_3_2_1_11_1","first-page":"164","volume-title":"An approach to formalization and analysis of message passing libraries. Formal Methods for Industrial Critical Systems (best paper). LNCS 4916","author":"Palmer Robert","year":"2008","unstructured":"Robert Palmer , Michael Delisi , Ganesh Gopalakrishnan , and Robert M. Kirby . An approach to formalization and analysis of message passing libraries. Formal Methods for Industrial Critical Systems (best paper). LNCS 4916 , pages 164 -- 181 , 2008 . Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, and Robert M. Kirby. An approach to formalization and analysis of message passing libraries. Formal Methods for Industrial Critical Systems (best paper). LNCS 4916, pages 164--181, 2008."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPPW.2010.33"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA538815"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"e_1_3_2_1_16_1","unstructured":"Yu Yang Xiaofang Chen Ganesh Gopalakrishnan and Robert Kirby. Runtime model checking of multi-threaded C\/C++ programs. TR UUCS-07-008.  Yu Yang Xiaofang Chen Ganesh Gopalakrishnan and Robert Kirby. Runtime model checking of multi-threaded C\/C++ programs. TR UUCS-07-008."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390841.1390844"},{"key":"e_1_3_2_1_18_1","volume-title":"School of Computing","author":"Vakkalanka Sarvani","year":"2010","unstructured":"Sarvani Vakkalanka , Ph D Dissertation , University of Utah , School of Computing , 2010 . http:\/\/www.cs.utah.edu\/~sarvani\/dissertation.html. Sarvani Vakkalanka, PhD Dissertation, University of Utah, School of Computing, 2010. http:\/\/www.cs.utah.edu\/~sarvani\/dissertation.html."},{"key":"e_1_3_2_1_19_1","volume-title":"Precise Dynamic Analysis for Slack Elasticity: Adding Buffering Without Adding Bugs. Accepted for presentation in EuroMPI","author":"Vakkalanka Sarvani","year":"2010","unstructured":"Sarvani Vakkalanka , Anh Vo , Ganesh Gopalakrishnan , and Robert M. Kirby . Precise Dynamic Analysis for Slack Elasticity: Adding Buffering Without Adding Bugs. Accepted for presentation in EuroMPI 2010 , Stuttgart , Germany, September, 2010. Sarvani Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, and Robert M. Kirby. Precise Dynamic Analysis for Slack Elasticity: Adding Buffering Without Adding Bugs. Accepted for presentation in EuroMPI 2010, Stuttgart, Germany, September, 2010."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1348250.1348256"}],"event":{"name":"SIGSOFT\/FSE'10: 18th ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Santa Fe New Mexico USA","acronym":"SIGSOFT\/FSE'10","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the FSE\/SDP workshop on Future of software engineering research"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1882362.1882392","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1882362.1882392","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:33Z","timestamp":1750244373000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1882362.1882392"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,7]]},"references-count":21,"alternative-id":["10.1145\/1882362.1882392","10.1145\/1882362"],"URL":"https:\/\/doi.org\/10.1145\/1882362.1882392","relation":{},"subject":[],"published":{"date-parts":[[2010,11,7]]},"assertion":[{"value":"2010-11-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}