{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:07:39Z","timestamp":1773655659409,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":92,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,27]],"date-time":"2020-06-27T00:00:00Z","timestamp":1593216000000},"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":[[2020,6,27]]},"DOI":"10.1145\/3377811.3380419","type":"proceedings-article","created":{"date-parts":[[2020,10,1]],"date-time":"2020-10-01T18:25:34Z","timestamp":1601576734000},"page":"1248-1260","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Symbolic verification of message passing interface programs"],"prefix":"10.1145","author":[{"given":"Hengbiao","family":"Yu","sequence":"first","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Zhenbang","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Xianjin","family":"Fu","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Zhendong","family":"Su","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore"}]},{"given":"Chun","family":"Huang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Wei","family":"Dong","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2020,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Allinea. 2002. Allinea DDT. http:\/\/www.allinea.com\/products\/ddt\/. (2002)."},{"key":"e_1_3_2_1_2_1","volume-title":"Rami G\u00f6khan Kici, and Ranjit Jhala","author":"Bakst Alexander","year":"2017","unstructured":"Alexander Bakst, Klaus von Gleissenthall, Rami G\u00f6khan Kici, and Ranjit Jhala. 2017. Verifying distributed programs via canonical sequentialization. PACMPL 1, OOPSLA (2017), 110:1--110:27."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Stanislav B\u00f6hm Ondrej Meca and Petr Jancar. 2016. State-Space Reduction of Non-deterministically Synchronizing Systems Applicable to Deadlock Detection in MPI. In FM. 102--118.","DOI":"10.1007\/978-3-319-48989-6_7"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Peter Boonstoppel Cristian Cadar and Dawson Engler. 2008. RWset: attacking path explosion in constraint-based test generation. In TACAS. 351--366.","DOI":"10.1007\/978-3-540-78800-3_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Vincent Botbol Emmanuel Chailloux and Tristan Le Gall. 2017. Static Analysis of Communicating Processes Using Symbolic Transducers. In VMCAI. 73--90.","DOI":"10.1007\/978-3-319-52234-0_5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103681"},{"key":"e_1_3_2_1_7_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. 372--391","author":"Bouajjani Ahmed","year":"2018","unstructured":"Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. 2018. On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II. 372--391."},{"key":"e_1_3_2_1_8_1","volume-title":"On communicating finite-state machines. J. ACM","author":"Brand Daniel","year":"1983","unstructured":"Daniel Brand and Pitro Zafiropulo. 1983. On communicating finite-state machines. J. ACM (1983), 323--342."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Greg Bronevetsky. 2009. Communication-sensitive static dataflow for parallel message passing applications. In CGO. 1--12.","DOI":"10.1109\/CGO.2009.32"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Stefan Bucur Vlad Ureche Cristian Zamfir and George Candea. 2011. Parallel symbolic execution for automated real-world software testing. In EuroSYS. 183--198.","DOI":"10.1145\/1966445.1966463"},{"key":"e_1_3_2_1_11_1","volume-title":"High performance cluster computing: architectures and systems","author":"Buyya Rajkumar","year":"1999","unstructured":"Rajkumar Buyya and others. 1999. High performance cluster computing: architectures and systems. Prentice Hall (1999), 999."},{"key":"e_1_3_2_1_12_1","volume-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI. 209--224.","author":"Cadar C.","year":"2008","unstructured":"C. Cadar, D. Dunbar, and D. Engler. 2008. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI. 209--224."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040026.56959.91"},{"key":"e_1_3_2_1_14_1","volume-title":"TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. 341--356","author":"Cimatti Alessandro","year":"2011","unstructured":"Alessandro Cimatti, Iman Narasamdya, and Marco Roveri. 2011. Boosting Lazy Abstraction for SystemC with Partial Order Reduction. In Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. 341--356."},{"key":"e_1_3_2_1_15_1","unstructured":"Clang. 2016. Clang Static Analyzer. http:\/\/clang-analyzer.llvm.org. (2016)."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Edmund Clarke Orna Grumberg Somesh Jha Yuan Lu and Helmut Veith. 2000. Counterexample-guided abstraction refinement. In CAV. 154--169.","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_17_1","volume-title":"Model checking","author":"Clarke Edmund M","unstructured":"Edmund M Clarke, Orna Grumberg, and Doron Peled. 1999. Model checking. MIT press."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Heming Cui Gang Hu Jingyue Wu and Junfeng Yang. 2013. Verifying systems rules using rule-directed symbolic execution. In ASPLOS. 329--342.","DOI":"10.1145\/2499368.2451152"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Przemys\u0142aw Daca Ashutosh Gupta and Thomas A Henzinger. 2016. Abstraction-driven Concolic Testing. In VMCAI. 328--347.","DOI":"10.1007\/978-3-662-49122-5_16"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_1_22_1","first-page":"1","article-title":"MPI-checker: static analysis for MPI","volume":"3","author":"Droste Alexander","year":"2015","unstructured":"Alexander Droste, Michael Kuhn, and Thomas Ludwig. 2015. MPI-checker: static analysis for MPI. In LLVM-HPC. 3:1--3:10.","journal-title":"LLVM-HPC."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Vojt\u011bch Forejt Daniel Kroening Ganesh Narayanaswamy and Subodh Sharma. 2014. Precise predictive analysis for discovering communication deadlocks in MPI programs. In FM. 263--278.","DOI":"10.1007\/978-3-319-06410-9_19"},{"key":"e_1_3_2_1_24_1","volume-title":"MPI: A Message-Passing Interface Standard Version 3.0","author":"Forum MPI","year":"2012","unstructured":"MPI Forum. 2012. MPI: A Message-Passing Interface Standard Version 3.0. http:\/\/mpi-forum.org. (2012)."},{"key":"e_1_3_2_1_25_1","volume-title":"MPISE: Symbolic Execution of MPI Programs. In HASE. 181--188.","author":"Fu Xianjin","year":"2015","unstructured":"Xianjin Fu, Zhenbang Chen, Yufeng Zhang, Chun Huang, Wei Dong, and Ji Wang. 2015. MPISE: Symbolic Execution of MPI Programs. In HASE. 181--188."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Edgar Gabriel Graham E Fagg George Bosilca Thara Angskun Jack J Dongarra Jeffrey M Squyres Vishal Sahay Prabhanjan Kambadur Brian Barrett Andrew Lumsdaine and others. 2004. Open MPI: Goals concept and design of a next generation MPI implementation. In EuroMPI. 97--104.","DOI":"10.1007\/978-3-540-30218-6_19"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Patrice Godefroid Nils Klarlund and Koushik Sen. 2005. DART: directed automated random testing. In PLDI. 213--223.","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_3_2_1_28_1","volume-title":"Molnar","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In NDSS."},{"key":"e_1_3_2_1_29_1","volume-title":"Report of the HPC Correctness Summit","author":"Gopalakrishnan Ganesh","year":"2017","unstructured":"Ganesh Gopalakrishnan, Paul D. Hovland, Costin Iancu, Sriram Krishnamoorthy, Ignacio Laguna, Richard A. Lethin, Koushik Sen, Stephen F. Siegel, and Armando Solar-Lezama. 2017. Report of the HPC Correctness Summit Jan 25-26, 2017, Washington, DC. https:\/\/science.energy.gov\/~\/media\/ascr\/pdf\/programdocuments\/docs\/2017\/HPC_Correctness_Report.pdf. (2017)."},{"key":"e_1_3_2_1_30_1","volume-title":"Formal analysis of MPI-based parallel programs. Commun. ACM","author":"Gopalakrishnan Ganesh","year":"2011","unstructured":"Ganesh Gopalakrishnan, Robert M. Kirby, Stephen F. Siegel, Rajeev Thakur, William Gropp, Ewing L. Lusk, Bronis R. de Supinski, Martin Schulz, and Greg Bronevetsky. 2011. Formal analysis of MPI-based parallel programs. Commun. ACM (2011), 82--91."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"William Gropp. 2002. MPICH2: A new start for MPI implementations. In EuroMPI. 7--7.","DOI":"10.1007\/3-540-45825-5_5"},{"key":"e_1_3_2_1_32_1","volume-title":"Using MPI: Portable Parallel Programming with the Message-Passing Interface","author":"Gropp William","unstructured":"William Gropp, Ewing Lusk, and Anthony Skjellum. 2014. Using MPI: Portable Parallel Programming with the Message-Passing Interface. The MIT Press."},{"key":"e_1_3_2_1_33_1","volume-title":"Using MPI-2: Advanced features of the message-passing interface","author":"Gropp William","unstructured":"William Gropp, Ewing Lusk, and Rajeev Thakur. 1999. Using MPI-2: Advanced features of the message-passing interface. MIT press."},{"key":"e_1_3_2_1_34_1","unstructured":"Shengjian Guo Markus Kusano Chao Wang Zijiang Yang and Aarti Gupta. 2015. Assertion guided symbolic execution of multithreaded programs. In FSE. 854--865."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236028"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Tobias Hilbrich Joachim Protze Martin Schulz Bronis R de Supinski and Matthias S M\u00fcller. 2012. MPI runtime error detection with MUST: advances in deadlock detection. In SC. 30.","DOI":"10.1109\/SC.2012.79"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_38_1","unstructured":"Gerard J. Holzmann. 2012. Promela manual pages. http:\/\/spinroot.com\/spin\/Man\/promela.html. (2012)."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462167"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Yu Huang and Eric Mercer. 2015. Detecting MPI Zero Buffer Incompatibility by SMT Encoding. In NFM. 219--233.","DOI":"10.1007\/978-3-319-17524-9_16"},{"key":"e_1_3_2_1_42_1","volume-title":"Lazy-CSeq: A Context-Bounded Model Checking Tool for Multithreaded C-Programs. In 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015","author":"Inverso Omar","year":"2015","unstructured":"Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2015. Lazy-CSeq: A Context-Bounded Model Checking Tool for Multithreaded C-Programs. In 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015. 807--812."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Joxan Jaffar Vijayaraghavan Murali and Jorge A Navas. 2013. Boosting concolic testing via interpolation. In FSE. 48--58.","DOI":"10.1145\/2491411.2491425"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Ranjit Jhala and Rupak Majumdar. 2005. Path slicing. In PLDI. 38--47.","DOI":"10.1145\/1064978.1065016"},{"key":"e_1_3_2_1_45_1","volume-title":"MCC","author":"Jiang Ke","year":"2009","unstructured":"Ke Jiang and Bengt Jonsson. 2009. Using SPIN to model check concurrent algorithms, using a translation from C to Promela. In MCC 2009. 67--69."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Ren\u00e9 Just Darioush Jalali Laura Inozemtseva Michael D Ernst Reid Holmes and Gordon Fraser. 2014. Are mutants a valid substitute for real faults in software testing?. In FSE. 654--665.","DOI":"10.1145\/2635868.2635929"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Dhriti Khanna Subodh Sharma C\u00e9sar Rodr\u00edguez and Rahul Purandare. 2018. Dynamic Symbolic Verification of MPI Programs. In FM.","DOI":"10.1007\/978-3-319-95582-7_28"},{"key":"e_1_3_2_1_48_1","volume-title":"Symbolic execution and program testing. Commun. ACM","author":"King J.C.","year":"1976","unstructured":"J.C. King. 1976. Symbolic execution and program testing. Commun. ACM (1976), 385--394."},{"key":"e_1_3_2_1_49_1","volume-title":"Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory, CONCUR 2018","author":"Kragl Bernhard","year":"2018","unstructured":"Bernhard Kragl, Shaz Qadeer, and Thomas A. Henzinger. 2018. Synchronizing the Asynchronous. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. 21:1--21:17."},{"key":"e_1_3_2_1_50_1","volume-title":"MARMOT: An MPI analysis and checking tool. Advances in Parallel Computing","author":"Krammer Bettina","year":"2004","unstructured":"Bettina Krammer, Katrin Bidmon, Matthias S M\u00fcller, and Michael M Resch. 2004. MARMOT: An MPI analysis and checking tool. Advances in Parallel Computing (2004), 493--500."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2667219"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302516.3307353"},{"key":"e_1_3_2_1_54_1","volume-title":"COMPI: Concolic Testing for MPI Applications. In 2018 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2018","author":"Li Hongbo","year":"2018","unstructured":"Hongbo Li, Sihuan Li, Zachary Benavides, Zizhong Chen, and Rajiv Gupta. 2018. COMPI: Concolic Testing for MPI Applications. In 2018 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2018, Vancouver, BC, Canada, May 21-25, 2018. 865--874."},{"key":"e_1_3_2_1_55_1","volume-title":"Vasco Thudichum Vasconcelos, and Nobuko Yoshida","author":"L\u00f3pez Hugo A.","year":"2015","unstructured":"Hugo A. L\u00f3pez, Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, C\u00e9sar Santos, Vasco Thudichum Vasconcelos, and Nobuko Yoshida. 2015. Protocol-based verification of message-passing parallel programs. In OOPSLA. 280--298."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.3113\/JSOA.2018.0261"},{"key":"e_1_3_2_1_57_1","first-page":"1","article-title":"Verification of MPI programs using CIVL","volume":"6","author":"Luo Ziqing","year":"2017","unstructured":"Ziqing Luo, Manchun Zheng, and Stephen F. Siegel. 2017. Verification of MPI programs using CIVL. In EuroMPI. 6:1--6:11.","journal-title":"EuroMPI."},{"key":"e_1_3_2_1_58_1","volume-title":"The temporal logic of reactive and concurrent systems - specification","author":"Manna Zohar","unstructured":"Zohar Manna and Amir Pnueli. 1992. The temporal logic of reactive and concurrent systems - specification. Springer."},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. 2005. Applications of Craig Interpolants in Model Checking. In TACAS. 1--12.","DOI":"10.1007\/978-3-540-31980-1_1"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594336"},{"key":"e_1_3_2_1_61_1","unstructured":"Matthias M\u00fcller Bronis de Supinski Ganesh Gopalakrishnan Tobias Hilbrich and David Lecomber. 2011. Dealing with MPI bugs at scale: Best practices automatic detection debugging and formal verification. http:\/\/sc11.supercomputing.org\/schedule\/event_detail.php?evid=tut131 (2011)."},{"key":"e_1_3_2_1_62_1","volume-title":"Piramanayagam Arumuga Nainar, and Iulian Neamtiu","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, G\u00e9rard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings. 267--280."},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892232"},{"key":"e_1_3_2_1_64_1","volume-title":"Principles of program analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson, Hanne R Nielson, and Chris Hankin. 2015. Principles of program analysis. Springer."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"crossref","unstructured":"Aditya V Nori Sriram K Rajamani SaiDeep Tetali and Aditya V Thakur. 2009. The YOGI Project: Software property checking via static analysis and testing. In TACAS. 178--181.","DOI":"10.1007\/978-3-642-00768-2_17"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Wojciech Penczek Maciej Szreter Rob Gerth and Ruurd Kuiper. 2000. Improving Partial Order Reductions for Universal Branching Time Properties. Fundam. Inform. (2000) 245--267.","DOI":"10.3233\/FI-2000-43123413"},{"key":"e_1_3_2_1_68_1","volume-title":"Engler","author":"Ramos David A.","year":"2015","unstructured":"David A. Ramos and Dawson R. Engler. 2015. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In SEC. USENIX Association, 49--64."},{"key":"e_1_3_2_1_69_1","volume-title":"Rico-Gallego and Juan Carlos D\u00edaz Mart\u00edn","author":"Juan","year":"2011","unstructured":"Juan A. Rico-Gallego and Juan Carlos D\u00edaz Mart\u00edn. 2011. Performance Evaluation of Thread-Based MPI in Shared Memory. In EuroMPI. 337--338."},{"key":"e_1_3_2_1_70_1","volume-title":"The theory and practice of concurrency","author":"Roscoe Bill","unstructured":"Bill Roscoe. 2005. The theory and practice of concurrency. Prentice-Hall."},{"key":"e_1_3_2_1_71_1","unstructured":"Victor Samofalov V. Krukov B. Kuhn S. Zheltov Alexander V. Konovalov and J. DeSouza. 2005. Automated Correctness Analysis of MPI Programs with Intel(r) Message Checker. In PARCO. 901--908."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_73_1","unstructured":"Stephen F. Siegel. Model Checking Nonblocking MPI Programs. In VMCAI."},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"crossref","unstructured":"Stephen F. Siegel. 2007. Verifying Parallel Programs with MPI-Spin. In PVM\/MPI. 13--14.","DOI":"10.1007\/978-3-540-75416-9_8"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_76_1","volume-title":"FEVS: A functional equivalence verification suite for high-performance scientific computing. Mathematics in Computer Science","author":"Siegel Stephen F","year":"2011","unstructured":"Stephen F Siegel and Timothy K Zirkel. 2011. FEVS: A functional equivalence verification suite for high-performance scientific computing. Mathematics in Computer Science (2011), 427--435."},{"key":"e_1_3_2_1_77_1","volume-title":"Zirkel","author":"Siegel Stephen F.","year":"2011","unstructured":"Stephen F. Siegel and Timothy K. Zirkel. 2011. TASS: The Toolkit for Accurate Scientific Software. Mathematics in Computer Science (2011), 395--426."},{"key":"e_1_3_2_1_78_1","volume-title":"MPI-the Complete Reference: The MPI core","author":"Snir Marc","unstructured":"Marc Snir. 1998. MPI-the Complete Reference: The MPI core. Vol. 1. MIT press."},{"key":"e_1_3_2_1_79_1","unstructured":"Ting Su Zhoulai Fu Geguang Pu Jifeng He and Zhendong Su. 2015. Combining symbolic execution and model checking for data flow testing. In ICSE. 654--665."},{"key":"e_1_3_2_1_80_1","volume-title":"Jin Song Dong, and Jun Pang","author":"Sun Jun","year":"2009","unstructured":"Jun Sun, Yang Liu, Jin Song Dong, and Jun Pang. 2009. PAT: Towards flexible verification under fairness. In CAV. 709--714."},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"crossref","unstructured":"Nikolai Tillmann and Jonathan de Halleux. 2008. Pex-White Box Test Generation for .NET. In TAP. 134--153.","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"e_1_3_2_1_83_1","volume-title":"Kirby","author":"Vakkalanka Sarvani S.","year":"2008","unstructured":"Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby. 2008. Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. In CAV. 66--79."},{"key":"e_1_3_2_1_84_1","volume-title":"Martin Schulz, and Greg Bronevetsky.","author":"Vo Anh","year":"2010","unstructured":"Anh Vo, Sriram Aananthakrishnan, Ganesh Gopalakrishnan, Bronis R De Supinski, Martin Schulz, and Greg Bronevetsky. 2010. A scalable and distributed dynamic formal verifier for MPI programs. In SC. 1--10."},{"key":"e_1_3_2_1_85_1","volume-title":"Alexander Bakst, Deian Stefan, and Ranjit Jhala.","author":"von Gleissenthall Klaus","year":"2019","unstructured":"Klaus von Gleissenthall, Rami G\u00f6khan Kici, Alexander Bakst, Deian Stefan, and Ranjit Jhala. 2019. Pretend synchrony: synchronous verification of asynchronous distributed programs. PACMPL 3, POPL (2019), 59:1--59:30."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180177"},{"key":"e_1_3_2_1_87_1","unstructured":"Rogue Wave. 2009. TotalView Software. http:\/\/www.roguewave.com\/products\/totalview. (2009)."},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594835.1504213"},{"key":"e_1_3_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2018.00066"},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_25"},{"key":"e_1_3_2_1_91_1","volume-title":"Combining Symbolic Execution and Model Checking to Verify MPI Programs. CoRR abs\/1803.06300","author":"Yu Hengbiao","year":"2020","unstructured":"Hengbiao Yu, Zhenbang Chen, Xianjin Fu, Ji Wang, Zhendong Su, Jun Sun, Chun Huang, and Wei Dong. 2020. Combining Symbolic Execution and Model Checking to Verify MPI Programs. CoRR abs\/1803.06300 (2020). arXiv:1803.06300 http:\/\/arxiv.org\/abs\/1803.06300"},{"key":"e_1_3_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180227"},{"key":"e_1_3_2_1_93_1","volume-title":"Regular property guided dynamic symbolic execution","author":"Zhang Yufeng","unstructured":"Yufeng Zhang, Zhenbang Chen, Ji Wang, Wei Dong, and Zhiming Liu. 2015. Regular property guided dynamic symbolic execution. In ICSE. IEEE Press, 643--653."}],"event":{"name":"ICSE '20: 42nd International Conference on Software Engineering","location":"Seoul South Korea","acronym":"ICSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","KIISE Korean Institute of Information Scientists and Engineers","IEEE CS"]},"container-title":["Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380419","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3377811.3380419","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:40Z","timestamp":1750200100000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3377811.3380419"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,27]]},"references-count":92,"alternative-id":["10.1145\/3377811.3380419","10.1145\/3377811"],"URL":"https:\/\/doi.org\/10.1145\/3377811.3380419","relation":{},"subject":[],"published":{"date-parts":[[2020,6,27]]},"assertion":[{"value":"2020-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}