{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:38Z","timestamp":1773655658762,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,10,23]],"date-time":"2015-10-23T00:00:00Z","timestamp":1445558400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["PTDC\/EIACCO\/122547,117513\/2010,UID\/CEC\/00408\/2013"],"award-info":[{"award-number":["PTDC\/EIACCO\/122547,117513\/2010,UID\/CEC\/00408\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K011715\/1,EP\/K034413\/1,EP\/L00058X\/1"],"award-info":[{"award-number":["EP\/K011715\/1,EP\/K034413\/1,EP\/L00058X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001732","name":"Danmarks Grundforskningsfond","doi-asserted-by":"publisher","award":["DNRF86-10"],"award-info":[{"award-number":["DNRF86-10"]}],"id":[{"id":"10.13039\/501100001732","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["IC1201 BETTY"],"award-info":[{"award-number":["IC1201 BETTY"]}],"id":[{"id":"10.13039\/501100000921","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["FP7-612985"],"award-info":[{"award-number":["FP7-612985"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,10,23]]},"DOI":"10.1145\/2814270.2814302","type":"proceedings-article","created":{"date-parts":[[2015,11,2]],"date-time":"2015-11-02T16:04:33Z","timestamp":1446480273000},"page":"280-298","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":29,"title":["Protocol-based verification of message-passing parallel programs"],"prefix":"10.1145","author":[{"given":"Hugo A.","family":"L\u00f3pez","sequence":"first","affiliation":[{"name":"DTU, Denmark"}]},{"given":"Eduardo R. B.","family":"Marques","sequence":"additional","affiliation":[{"name":"University of Lisbon, Portugal"}]},{"given":"Francisco","family":"Martins","sequence":"additional","affiliation":[{"name":"University of Lisbon, Portugal"}]},{"given":"Nicholas","family":"Ng","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"C\u00e9sar","family":"Santos","sequence":"additional","affiliation":[{"name":"University of Lisbon, Portugal"}]},{"given":"Vasco Thudichum","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"University of Lisbon, Portugal"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2015,10,23]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2464996.2467286"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_2_3_1","volume-title":"CUP","author":"Coquand T.","year":"1991","unstructured":"T. Coquand . Logical Frameworks, chapter An algorithm for testing conversion in type theory . CUP , 1991 . T. Coquand. Logical Frameworks, chapter An algorithm for testing conversion in type theory. CUP, 1991."},{"key":"e_1_3_2_2_4_1","first-page":"337","volume":"4963","author":"de Moura L. M.","year":"2008","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: An efficient SMT solver. In TACAS , volume 4963 of LNCS, pages 337 \u2013 340 . Springer, 2008 . L. M. de Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer, 2008.","journal-title":"Z3: An efficient SMT solver. In TACAS"},{"key":"e_1_3_2_2_5_1","volume-title":"Parameterised multiparty session types. Logical Methods in Computer Science, 8(4)","author":"Deni\u00e9lou P.","year":"2012","unstructured":"P. Deni\u00e9lou , N. Yoshida , A. Bejleri , and R. Hu . Parameterised multiparty session types. Logical Methods in Computer Science, 8(4) , 2012 . P. Deni\u00e9lou, N. Yoshida, A. Bejleri, and R. Hu. Parameterised multiparty session types. Logical Methods in Computer Science, 8(4), 2012."},{"key":"e_1_3_2_2_6_1","first-page":"263","volume":"8442","author":"Forejt V.","year":"2014","unstructured":"V. Forejt , D. Kroening , G. Narayanswamy , and S. Sharma . Precise predictive analysis for discovering communication deadlocks in MPI programs. In FM , volume 8442 of LNCS, pages 263 \u2013 278 . Springer, 2014 . V. Forejt, D. Kroening, G. Narayanswamy, and S. Sharma. Precise predictive analysis for discovering communication deadlocks in MPI programs. In FM, volume 8442 of LNCS, pages 263\u2013278. Springer, 2014.","journal-title":"In FM"},{"key":"e_1_3_2_2_7_1","volume-title":"MPI: A Message-Passing Interface Standard\u2014 Version 3.0","author":"Forum M.","year":"2012","unstructured":"M. Forum . MPI: A Message-Passing Interface Standard\u2014 Version 3.0 . High-Performance Computing Center Stuttgart , 2012 . M. Forum. MPI: A Message-Passing Interface Standard\u2014 Version 3.0. High-Performance Computing Center Stuttgart, 2012."},{"key":"e_1_3_2_2_8_1","volume-title":"Addison-Wesley","author":"Foster I.","year":"1995","unstructured":"I. Foster . Designing and building parallel programs . Addison-Wesley , 1995 . I. Foster. Designing and building parallel programs. Addison-Wesley, 1995."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297033"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043194"},{"key":"e_1_3_2_2_11_1","first-page":"104","volume-title":"International Summer School Logics and Languages for Reliability and Security","author":"Gordon A. D.","unstructured":"A. D. Gordon and C. Fournet . Principles and applications of refinement types . In International Summer School Logics and Languages for Reliability and Security , pages 73\u2013 104 . IOS Press, 2010. A. D. Gordon and C. Fournet. Principles and applications of refinement types. In International Summer School Logics and Languages for Reliability and Security, pages 73\u2013104. IOS Press, 2010."},{"key":"e_1_3_2_2_12_1","series-title":"Scientific and Engineering Computation series","volume-title":"Using MPI: portable parallel programming with the message passing interface","author":"Gropp W.","year":"1999","unstructured":"W. Gropp , E. Lusk , and A. Skjellum . Using MPI: portable parallel programming with the message passing interface . Scientific and Engineering Computation series . MIT press , 1999 . W. Gropp, E. Lusk, and A. Skjellum. Using MPI: portable parallel programming with the message passing interface. Scientific and Engineering Computation series. MIT press, 1999."},{"key":"e_1_3_2_2_13_1","first-page":"1","volume":"30","author":"Hilbrich T.","year":"2012","unstructured":"T. Hilbrich , J. Protze , M. Schulz , B. R. de Supinski , and M. S. M\u00fcller . MPI runtime error detection with MUST: advances in deadlock detection. In SC, pages 30 : 1 \u2013 30 :11. IEEE\/ACM, 2012 . T. Hilbrich, J. Protze, M. Schulz, B. R. de Supinski, and M. S. M\u00fcller. MPI runtime error detection with MUST: advances in deadlock detection. In SC, pages 30:1\u201330:11. IEEE\/ACM, 2012.","journal-title":"In SC, pages"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_2_2_15_1","series-title":"LNCS","first-page":"75","volume-title":"ICDCIT","author":"Honda K.","unstructured":"K. Honda , A. Mukhamedov , G. Brown , T. Chen , and N. Yoshida . Scribbling interactions with a formal foundation . In ICDCIT , volume 6536 of LNCS , pages 55\u2013 75 . Springer, 2011. K. Honda, A. Mukhamedov, G. Brown, T. Chen, and N. Yoshida. Scribbling interactions with a formal foundation. In ICDCIT, volume 6536 of LNCS, pages 55\u201375. Springer, 2011."},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33518-1_37"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44471-9_5"},{"key":"e_1_3_2_2_18_1","first-page":"36","volume-title":"ASE","author":"Huang Y.","unstructured":"Y. Huang , E. Mercer , and J. McCarthy . Proving MCAPI executions are correct using SMT . In ASE , pages 26\u2013 36 . IEEE, 2013. Y. Huang, E. Mercer, and J. McCarthy. Proving MCAPI executions are correct using SMT. In ASE, pages 26\u201336. IEEE, 2013."},{"key":"e_1_3_2_2_19_1","first-page":"25","volume":"155","author":"Kouzapas D.","year":"2014","unstructured":"D. Kouzapas , R. Gutkovas , and S. J. Gay . Session types for broadcasting. In PLACES , volume 155 of EPTCS, pages 25 \u2013 31 , 2014 . D. Kouzapas, R. Gutkovas, and S. J. Gay. Session types for broadcasting. In PLACES, volume 155 of EPTCS, pages 25\u201331, 2014.","journal-title":"Session types for broadcasting. In PLACES"},{"key":"e_1_3_2_2_20_1","volume-title":"Department of Informatics","author":"Lemos F.","year":"2014","unstructured":"F. Lemos . Synthesis of correct-by-construction MPI programs. Master\u2019s thesis , Department of Informatics , University of Lisbon , 2014 . F. Lemos. Synthesis of correct-by-construction MPI programs. Master\u2019s thesis, Department of Informatics, University of Lisbon, 2014."},{"key":"e_1_3_2_2_21_1","first-page":"103","volume":"137","author":"Marques E. R. B.","year":"2013","unstructured":"E. R. B. Marques , F. Martins , V. T. Vasconcelos , N. Ng , and N. Martins . Towards deductive verification of MPI programs against session types. In PLACES , volume 137 of EPTCS, pages 103 \u2013 113 , 2013 . E. R. B. Marques, F. Martins, V. T. Vasconcelos, N. Ng, and N. Martins. Towards deductive verification of MPI programs against session types. In PLACES, volume 137 of EPTCS, pages 103\u2013113, 2013.","journal-title":"In PLACES"},{"key":"e_1_3_2_2_22_1","volume-title":"Bibliopolis-Napoli","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"P. Martin-L\u00f6f . Intuitionistic Type Theory . Bibliopolis-Napoli , 1984 . P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis-Napoli, 1984."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11761-014-0172-8"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_11"},{"key":"e_1_3_2_2_26_1","volume-title":"Morgan Kaufmann","author":"Pacheco P.","year":"1997","unstructured":"P. Pacheco . Parallel programming with MPI . Morgan Kaufmann , 1997 . P. Pacheco. Parallel programming with MPI. Morgan Kaufmann, 1997."},{"key":"e_1_3_2_2_27_1","unstructured":"ParTypes. Partypes homepage. http:\/\/gloss.di.fc.ul.pt\/ParTypes July 2015.  ParTypes. Partypes homepage. http:\/\/gloss.di.fc.ul.pt\/ParTypes July 2015."},{"key":"e_1_3_2_2_28_1","first-page":"344","volume":"4757","author":"Pervez S.","year":"2007","unstructured":"S. Pervez , G. Gopalakrishnan , R. M. Kirby , R. Palmer , R. Thakur , and W. Gropp . Practical model-checking method for verifying correctness of MPI programs. In PVM\/MPI , volume 4757 of LNCS, pages 344 \u2013 353 . Springer, 2007 . S. Pervez, G. Gopalakrishnan, R. M. Kirby, R. Palmer, R. Thakur, and W. Gropp. Practical model-checking method for verifying correctness of MPI programs. In PVM\/MPI, volume 4757 of LNCS, pages 344\u2013353. Springer, 2007.","journal-title":"In PVM\/MPI"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.189.11"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2006.6"},{"key":"e_1_3_2_2_33_1","unstructured":"Scribble. Scribble homepage. http:\/\/www.scribble.org\/ July 2015.  Scribble. Scribble homepage. http:\/\/www.scribble.org\/ July 2015."},{"key":"e_1_3_2_2_34_1","first-page":"158","volume":"5161","author":"Sheard T.","year":"2007","unstructured":"T. Sheard and N. Linger . Programming in Omega. In CEFP , volume 5161 of LNCS, pages 158 \u2013 227 . Springer, 2007 . T. Sheard and N. Linger. Programming in Omega. In CEFP, volume 5161 of LNCS, pages 158\u2013227. Springer, 2007.","journal-title":"Programming in Omega. In CEFP"},{"key":"e_1_3_2_2_35_1","first-page":"2","volume":"6538","author":"Siegel S. F.","year":"2011","unstructured":"S. F. Siegel and G. Gopalakrishnan . Formal analysis of message passing. In VMCAI , volume 6538 of LNCS, pages 2 \u2013 18 . Springer, 2011 . S. F. Siegel and G. Gopalakrishnan. Formal analysis of message passing. In VMCAI, volume 6538 of LNCS, pages 2\u201318. Springer, 2011.","journal-title":"Formal analysis of message passing. In VMCAI"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87475-1_37"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-011-0101-6"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_27"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2010.7"},{"key":"e_1_3_2_2_41_1","first-page":"387","volume-title":"LICS","author":"Xi H.","unstructured":"H. Xi . Imperative programming with dependent types . In LICS , pages 375\u2013 387 . IEEE, 2000. H. Xi. Imperative programming with dependent types. In LICS, pages 375\u2013387. IEEE, 2000."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_3_2_2_43_1","first-page":"22","volume":"8358","author":"Yoshida N.","year":"2013","unstructured":"N. Yoshida , R. Hu , R. Neykova , and N. Ng . The Scribble protocol language. In TGC , volume 8358 of LNCS, pages 22 \u2013 41 . Springer, 2013 . N. Yoshida, R. Hu, R. Neykova, and N. Ng. The Scribble protocol language. In TGC, volume 8358 of LNCS, pages 22\u201341. Springer, 2013.","journal-title":"The Scribble protocol language. In TGC"}],"event":{"name":"SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Pittsburgh PA USA","acronym":"SPLASH '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814270.2814302","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2814270.2814302","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:48:41Z","timestamp":1750211321000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2814270.2814302"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10,23]]},"references-count":43,"alternative-id":["10.1145\/2814270.2814302","10.1145\/2814270"],"URL":"https:\/\/doi.org\/10.1145\/2814270.2814302","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2858965.2814302","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,10,23]]},"assertion":[{"value":"2015-10-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}