{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T04:34:29Z","timestamp":1742358869809,"version":"3.40.1"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_22","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T07:29:29Z","timestamp":1326958169000},"page":"332-347","source":"Crossref","is-referenced-by-count":2,"title":["Modeling Asynchronous Message Passing for C Programs"],"prefix":"10.1007","author":[{"given":"Everett","family":"Morse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nick","family":"Vrvilo","sequence":"additional","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":"297","reference":[{"key":"22_CR1","unstructured":"The 4M modeling language, https:\/\/github.com\/ericmercer\/4M"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B-book: assigning programs to meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1145\/361179.361202","volume":"17","author":"E.W. Dijkstra","year":"1974","unstructured":"Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Communications of the ACM\u00a017, 643\u2013644 (1974)","journal-title":"Communications of the ACM"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-15643-4_27","volume-title":"Automated Technology for Verification and Analysis","author":"M. Elwakil","year":"2010","unstructured":"Elwakil, M., Yang, Z.: CRI: Symbolic Debugger for MCAPI Applications. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 353\u2013358. Springer, Heidelberg (2010)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Elwakil, M., Yang, Z.: Debugging support tool for MCAPI applications. In: Parallel and Distributed Systems (2010)","DOI":"10.1145\/1866210.1866212"},{"key":"22_CR7","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. The MIT Press (2009)"},{"key":"22_CR8","unstructured":"Flatt, M.: PLT: Reference: Racket. Tech. Rep. PLT-TR-2010-1, PLT Inc. (2010), http:\/\/racket-lang.org\/tr1\/"},{"key":"22_CR9","unstructured":"Georgelin, P., Pierre, L., Nguyen, T.: A formal specification of the MPI primitives and communication mechanisms. Tech. rep., LIM (1999)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: Principles of Programming Languages, pp. 174\u2013186 (1997)","DOI":"10.1145\/263699.263717"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023, 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR12","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (April 2006)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-14977-1_17","volume-title":"Computational Logic in Multi-Agent Systems","author":"S.-S.T.Q. Jongmans","year":"2010","unstructured":"Jongmans, S.-S.T.Q., Hindriks, K.V., van Riemsdijk, M.B.: Model Checking Agent Programs by Using the Program Interpreter. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) CLIMA XI. LNCS, vol.\u00a06245, pp. 219\u2013237. Springer, Heidelberg (2010)"},{"key":"22_CR14","unstructured":"Lamport, L.: TLA - the temporal logic of actions, http:\/\/research.microsoft.com\/users\/lamport\/tla\/tla.html"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Li, G., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: Formal specification of the MPI-2.0 standard in TLA+. In: Principles and Practices of Parallel Programming, pp. 283\u2013284 (2008)","DOI":"10.1145\/1345206.1345257"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G., Kirby, R.M., Quinlan, D.: A symbolic verifier for CUDA programs. In: Principles and Practice of Parallel Programming, pp. 357\u2013358 (2010)","DOI":"10.1145\/1837853.1693512"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking: An approach to the state explosion problem. Ph.D. thesis, Carnegie Mellon University (1992)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/11537328_20","volume-title":"Model Checking Software","author":"E.G. Mercer","year":"2005","unstructured":"Mercer, E.G., Jones, M.: Model Checking Machine Code with the GNU Debugger. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol.\u00a03639, pp. 251\u2013265. Springer, Heidelberg (2005)"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Programming Language Design and Implementation (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-79707-4_13","volume-title":"Formal Methods for Industrial Critical Systems","author":"R. Palmer","year":"2008","unstructured":"Palmer, R., DeLisi, M., Gopalakrishnan, G., Kirby, R.M.: An Approach to Formalization and Analysis of Message Passing Libraries. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 164\u2013181. Springer, Heidelberg (2008)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"P\u01ces\u01cereanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: International Symposium on Software Testing and Analysis, pp. 15\u201326 (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"22_CR22","first-page":"353","volume-title":"Model-checking CSP","author":"A.W. Roscoe","year":"1994","unstructured":"Roscoe, A.W.: Model-checking CSP, pp. 353\u2013378. Prentice Hall International (UK) Ltd., Hertfordshire (1994)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Sharma, S., Gopalakrishnan, G., Mercer, E., Holt, J.: MCC: A runtime verification tool for MCAPI user applications. In: Formal Methods in Computer-Aided Design, pp. 41\u201344 (2009)","DOI":"10.1109\/FMCAD.2009.5351145"},{"key":"22_CR24","unstructured":"Siegel, S.F., Avrunin, G.: Analysis of mpi programs. Tech. Rep. UM-CS-2003-036, Department of Computer Science, University of Massachusetts Amherst (2003)"},{"key":"22_CR25","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall International Series In Computer Science, p. 155 (1989)"},{"key":"22_CR26","unstructured":"The Multicore Association, http:\/\/www.multicore-association.org"},{"key":"22_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-70545-1_9","volume-title":"Computer Aided Verification","author":"S. Vakkalanka","year":"2008","unstructured":"Vakkalanka, S., Gopalakrishnan, G., Kirby, R.M.: Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 66\u201379. Springer, Heidelberg (2008)"},{"key":"22_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-22306-8_14","volume-title":"Model Checking Software","author":"J. \u0160im\u0161a","year":"2011","unstructured":"\u0160im\u0161a, J., Bryant, R., Gibson, G.: dBug: Systematic Testing of Unmodified Distributed and Multi-threaded Systems. In: Groce, A., Musuvathi, M. (eds.) SPIN Workshops 2011. LNCS, vol.\u00a06823, pp. 188\u2013193. Springer, Heidelberg (2011)"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic pruning of concurrent program executions. In: The Foundations of Software Engineering, pp. 23\u201332 (2009)","DOI":"10.1145\/1595696.1595702"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-88387-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"C. Wang","year":"2008","unstructured":"Wang, C., Yang, Y., Gupta, A., Gopalakrishnan, G.: Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions. In: Cha, S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 126\u2013140. Springer, Heidelberg (2008)"},{"key":"22_CR31","unstructured":"Yang, J., Chen, T., Wu, M., Xu, Z., Liu, X., Lin, H., Yang, M., Long, F., Zhang, L., Zhou, L.: MODIST: transparent model checking of unmodified distributed systems. In: Networked Systems Design and Implementation, pp. 213\u2013228 (2009)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,18]],"date-time":"2025-03-18T23:25:29Z","timestamp":1742340329000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}