{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:28:12Z","timestamp":1746289692092,"version":"3.28.0"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,11]]},"DOI":"10.1109\/ase.2013.6693063","type":"proceedings-article","created":{"date-parts":[[2014,1,6]],"date-time":"2014-01-06T17:07:25Z","timestamp":1389028045000},"page":"26-36","source":"Crossref","is-referenced-by-count":8,"title":["Proving MCAPI executions are correct using SMT"],"prefix":"10.1109","author":[{"given":"Yu","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jay","family":"McCarthy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/238020.238033"},{"key":"17","first-page":"337","article-title":"Z3: An efficient SMT solver","volume":"4963","author":"de moura","year":"2008","journal-title":"TACAS"},{"journal-title":"MPPTest MPPTest Benchmark","year":"0","key":"18"},{"journal-title":"MCA The Multicore Association Resource Management API","year":"0","key":"15"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_22"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"journal-title":"MCA The Multicore Association","year":"0","key":"14"},{"key":"11","first-page":"398","article-title":"Monotonic partial order reduction: An optimal symbolic partial order reduction technique","author":"kahlon","year":"2009","journal-title":"ACM CAV"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_3"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351145"},{"journal-title":"Private Conversation on Active Research","year":"0","author":"sharma","key":"20"},{"key":"22","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-3-540-75416-9_8","article-title":"Verifying parallel programs with MPI-Spin","volume":"4757","author":"siegel","year":"2007","journal-title":"Lecture Notes in Computer Science"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_2"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941603"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_27"},{"key":"26","first-page":"724","article-title":"Reduced execution semantics of MPI: From theory to pratice","author":"vakkalanka","year":"2009","journal-title":"FM"},{"key":"27","first-page":"175","article-title":"Isp tool update: Scalable MPI verification","author":"vo","year":"2009","journal-title":"Parallel Tools Workshop"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/1595696.1595702"},{"key":"29","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1145\/1229428.1229472","article-title":"Barrier matching for programs with textually unaligned barriers","author":"zhang","year":"2007","journal-title":"Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming PPOPP"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2005.86"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"journal-title":"Proving MCAPI Executions Are Correct Using SMT (Extended)","year":"0","author":"huang","key":"10"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.32"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/1866210.1866212"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15643-4_27"},{"key":"5","first-page":"81","article-title":"A fast linear-arithmetic solver for DPLL(T)","volume":"4144","author":"dutertre","year":"2006","journal-title":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.005"},{"key":"9","article-title":"Targeting complex embedded architectures by combining the multicore communications API (MCAPI) with compiletime virtualisation","author":"gray","year":"2011","journal-title":"LCTES"},{"key":"8","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1145\/1040305.1040315","article-title":"Dynamic partial-order reduction for modeling checking software","author":"flanagan","year":"2005","journal-title":"POPL"}],"event":{"name":"2013 IEEE\/ACM 28th International Conference on Automated Software Engineering (ASE)","start":{"date-parts":[[2013,11,11]]},"location":"Silicon Valley, CA, USA","end":{"date-parts":[[2013,11,15]]}},"container-title":["2013 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6684409\/6693054\/06693063.pdf?arnumber=6693063","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,19]],"date-time":"2023-07-19T15:01:59Z","timestamp":1689778919000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6693063\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/ase.2013.6693063","relation":{},"subject":[],"published":{"date-parts":[[2013,11]]}}}