{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:30Z","timestamp":1781238930426,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,11,15]],"date-time":"2016-11-15T00:00:00Z","timestamp":1479168000000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1319571,CCF-1346769,CCF-0953210"],"award-info":[{"award-number":["CCF-1319571,CCF-1346769,CCF-0953210"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0012566"],"award-info":[{"award-number":["DE-SC0012566"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,11,15]]},"DOI":"10.1145\/2807591.2807635","type":"proceedings-article","created":{"date-parts":[[2015,10,27]],"date-time":"2015-10-27T09:07:31Z","timestamp":1445936851000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["CIVL"],"prefix":"10.1145","author":[{"given":"Stephen F.","family":"Siegel","sequence":"first","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Manchun","family":"Zheng","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ziqing","family":"Luo","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Timothy K.","family":"Zirkel","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andre V.","family":"Marianiello","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John G.","family":"Edenhofner","sequence":"additional","affiliation":[{"name":"University of Delaware"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew B.","family":"Dwyer","sequence":"additional","affiliation":[{"name":"University of Nebraska, Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael S.","family":"Rogers","sequence":"additional","affiliation":[{"name":"University of Nebraska, Lincoln"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,11,15]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Accessed","author":"ABC","year":"2015","unstructured":"ABC: ANTLR-Based C front-end. http:\/\/vsl.cis.udel.edu\/abc. Accessed Jul. 28, 2015."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/229883"},{"key":"e_1_3_2_1_4_1","volume-title":"Denver","author":"Balaji P.","year":"2013","unstructured":"P. Balaji, J. Dinan, T. Hoefler, and R. Thakur. Advanced MPI programming. Tutorial at SC13: International Conference on High Performance Computing, Networking, Storage, and Analysis, Denver, Colorado, November 2013. Accessed Feb. 6, 2015."},{"key":"e_1_3_2_1_5_1","first-page":"863","volume-title":"Proceedings of CAV","author":"Barnat J.","year":"2013","unstructured":"J. Barnat, L. Brim, V. Havel, J. Havl\u00edcek, J. Kriho, M. Lenco, P. Rockai, V. Still, and J. Weiser. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In N. Sharygina and H. Veith, editors, Proceedings of CAV, pages 863--868, 2013."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770397"},{"key":"e_1_3_2_1_8_1","volume-title":"http:\/\/people.sc.fsu.edu\/~jburkardt\/c_src\/openmp\/openmp.html. Accessed","author":"C","year":"2015","unstructured":"C OpenMP examples. http:\/\/people.sc.fsu.edu\/~jburkardt\/c_src\/openmp\/openmp.html. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_9_1","volume-title":"Accessed","author":"Center for Development of Advanced Computing. hyPACK","year":"2013","unstructured":"Center for Development of Advanced Computing. hyPACK 2013: MPI-OpenMP Programs. http:\/\/cdac.in\/index.aspx?id=ev_hpc_hypack_mpi_openmp_programs. Accessed Apr. 17, 2015."},{"key":"e_1_3_2_1_10_1","volume-title":"Accessed","author":"Center for Development of Advanced Computing.","year":"2015","unstructured":"Center for Development of Advanced Computing. Programming on Multi-Core Processors Using MPI - Pthreads. http:\/\/cdac.in\/index.aspx?id=ev_hpc_hypack_mpi_pthreads overview. Accessed Apr. 17, 2015."},{"key":"e_1_3_2_1_11_1","volume-title":"http:\/\/chapel.cray.com\/. Accessed","author":"The Chapel","year":"2015","unstructured":"The Chapel parallel programming language. http:\/\/chapel.cray.com\/. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370966"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_3_2_1_14_1","volume-title":"http:\/\/docs.nvidia.com\/cuda\/cuda-samples\/. Accessed","author":"Samples CUDA","year":"2015","unstructured":"CUDA Samples. http:\/\/docs.nvidia.com\/cuda\/cuda-samples\/. Accessed Apr. 15, 2015."},{"key":"e_1_3_2_1_15_1","volume-title":"http:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/. Accessed","author":"Programming Guide CUDA","year":"2015","unstructured":"CUDA Programming Guide Version 5.0. http:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040028.49845.67"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_46"},{"key":"e_1_3_2_1_20_1","unstructured":"M. Flatt and PLT. The Racket reference version 5.3.1. http:\/\/docs.racket-lang.org\/reference\/. Accessed Feb. 6 2015."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277725"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/2388996.2389087"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043194"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.102.11"},{"key":"e_1_3_2_1_26_1","volume-title":"Addison-Wesley","author":"Holzmann G. J.","year":"2004","unstructured":"G. J. Holzmann. The Spin Model Checker. Addison-Wesley, Boston, 2004."},{"key":"e_1_3_2_1_27_1","unstructured":"Institute of Electrical and Electronics Engineers Inc. IEEE Standard for Information Technology---Portable Operating System Interface (POSIX) Base Specifications Issue 7 IEEE Std 1003.1-2008 (Revision of IEEE Std 1003.1-2004). IEEE 3 Park Avenue New York NY 10016-5997 USA Dec. 2008."},{"key":"e_1_3_2_1_28_1","unstructured":"International Organization for Standardization and International Electrotechnical Commission. ISO\/IEC 989:2011 N1570: Programming Languages -- C. http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1570.pdf Apr. 2011."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_31_1","volume-title":"https:\/\/computing.llnl.gov\/tutorials\/mpi\/exercise.html. Accessed","author":"Lawrence Livermore National Laboratory Message-Passing Interface (MPI) exercise.","year":"2015","unstructured":"Lawrence Livermore National Laboratory Message-Passing Interface (MPI) exercise. https:\/\/computing.llnl.gov\/tutorials\/mpi\/exercise.html. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_32_1","volume-title":"https:\/\/computing.llnl.gov\/tutorials\/openMP\/exercise.html. Accessed","author":"Lawrence Livermore National Laboratory OpenMP tutorial.","year":"2015","unstructured":"Lawrence Livermore National Laboratory OpenMP tutorial. https:\/\/computing.llnl.gov\/tutorials\/openMP\/exercise.html. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_33_1","volume-title":"https:\/\/computing.llnl.gov\/tutorials\/pthreads\/exercise.html. Accessed","author":"Lawrence Livermore National Laboratory Pthreads tutorial.","year":"2015","unstructured":"Lawrence Livermore National Laboratory Pthreads tutorial. https:\/\/computing.llnl.gov\/tutorials\/pthreads\/exercise.html. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_34_1","unstructured":"K. R. M. Leino. This is Boogie 2. http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=147643 June 2008."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2014.20"},{"key":"e_1_3_2_1_37_1","unstructured":"Message-Passing Interface Forum. MPI: A Message-Passing Interface standard version 3.0. http:\/\/www.mpi-forum.org\/docs\/docs.html Sept. 2012."},{"key":"e_1_3_2_1_38_1","unstructured":"OpenMP Architecture Review Board. OpenMP API Specification for Parallel Programming. http:\/\/openmp.org\/wp\/. Accessed Feb. 8 2015."},{"key":"e_1_3_2_1_39_1","volume-title":"http:\/\/www.parasail-lang.org. Accessed","author":"Programming Language ParaSail","year":"2014","unstructured":"ParaSail Programming Language. http:\/\/www.parasail-lang.org. Accessed Feb. 7, 2014."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_41_1","volume-title":"http:\/\/users.abo.fi\/mats\/PP2014\/examples\/OpenMP\/omp_critical.c. Accessed","author":"Parallel","year":"2015","unstructured":"Parallel programming course. http:\/\/users.abo.fi\/mats\/PP2014\/examples\/OpenMP\/omp_critical.c. Accessed Feb. 8, 2015."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.342135"},{"key":"e_1_3_2_1_43_1","volume-title":"Information Technology: Research Computing. Carter -- User Guide. https:\/\/www.rcac.purdue.edu\/compute\/carter\/guide\/#compile_gpu","author":"Purdue University","year":"2008","unstructured":"Purdue University, Information Technology: Research Computing. Carter -- User Guide. https:\/\/www.rcac.purdue.edu\/compute\/carter\/guide\/#compile_gpu, 2008. Accessed Feb. 6, 2015."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1211440"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/361011.361061"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891996"},{"key":"e_1_3_2_1_48_1","unstructured":"SARL: The Symbolic Algebra and Reasoning Library. http:\/\/vsl.cis.udel.edu\/sarl Accessed Feb. 6 2015."},{"key":"e_1_3_2_1_49_1","unstructured":"S. F. Siegel and T. K. Zirkel. A Functional Equivalence Verification Suite. http:\/\/vsl.cis.udel.edu\/fevs. Accessed Feb. 6 2015."},{"issue":"4","key":"e_1_3_2_1_50_1","first-page":"395","volume":"5","author":"Siegel S. F.","year":"2011","unstructured":"S. F. Siegel and T. K. Zirkel. TASS: The Toolkit for Accurate Scientific Software. Mathematics in Computer Science, 5(4):395--426, 2011.","journal-title":"TASS: The Toolkit for Accurate Scientific Software. Mathematics in Computer Science"},{"key":"e_1_3_2_1_51_1","volume-title":"Using the GNU Compiler Collection: For GCC version 4.7.2","author":"Stallman R. M.","year":"2010","unstructured":"R. M. Stallman and the GCC Developer Community. Using the GNU Compiler Collection: For GCC version 4.7.2. GNU Press, a division of the Free Software Foundation, 2010. http:\/\/gcc.gnu.org\/onlinedocs\/gcc. Accessed Feb. 6, 2015."},{"key":"e_1_3_2_1_52_1","unstructured":"SV-COMP 2015: Competition on software verification. http:\/\/sv-comp.sosy-lab.org\/2015 Accessed Feb. 7 2015."},{"key":"e_1_3_2_1_53_1","unstructured":"VirginiaTech: Advanced Research Computing. CUDA. http:\/\/www.arc.vt.edu\/resources\/software\/cuda. Accessed Feb. 6 2015."},{"key":"e_1_3_2_1_54_1","volume-title":"http:\/\/research.microsoft.com\/en-us\/projects\/zing\/zinglanguagespecification.pdf","author":"Zing","year":"2005","unstructured":"Zing language specification, Microsoft Corporation. http:\/\/research.microsoft.com\/en-us\/projects\/zing\/zinglanguagespecification.pdf, 2005."},{"key":"e_1_3_2_1_55_1","first-page":"198","volume-title":"Proceedings of NFM","author":"Zirkel T. K.","year":"2013","unstructured":"T. K. Zirkel, S. F. Siegel, and T. McClory. Automated verification of Chapel programs using model checking and symbolic execution. In G. Brat, N. Rungta, and A. Venet, editors, Proceedings of NFM, pages 198--212, 2013."}],"event":{"name":"SC15: The International Conference for High Performance Computing, Networking, Storage and Analysis","location":"Austin Texas","acronym":"SC15","sponsor":["SIGHPC ACM Special Interest Group on High Performance Computing, Special Interest Group on High Performance Computing","SIGARCH ACM Special Interest Group on Computer Architecture","IEEE-CS Computer Society"]},"container-title":["Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2807591.2807635","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2807591.2807635","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2807591.2807635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:44:04Z","timestamp":1763459044000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2807591.2807635"}},"subtitle":["the concurrency intermediate verification language"],"short-title":[],"issued":{"date-parts":[[2015,11,15]]},"references-count":55,"alternative-id":["10.1145\/2807591.2807635","10.1145\/2807591"],"URL":"https:\/\/doi.org\/10.1145\/2807591.2807635","relation":{},"subject":[],"published":{"date-parts":[[2015,11,15]]},"assertion":[{"value":"2015-11-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}