{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:14:13Z","timestamp":1760044453595},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255398"},{"type":"electronic","value":"9783030255404"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25540-4_22","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:02:35Z","timestamp":1562929355000},"page":"387-397","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Cerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential C"],"prefix":"10.1007","author":[{"given":"Stella","family":"Lau","sequence":"first","affiliation":[]},{"given":"Victor B. F.","family":"Gomes","sequence":"additional","affiliation":[]},{"given":"Kayvan","family":"Memarian","sequence":"additional","affiliation":[]},{"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"22_CR1","unstructured":"CppMem: Interactive C\/C++ memory model. \n                      http:\/\/svr-pes20-cppmem.cl.cam.ac.uk\/cppmem\/index.html"},{"key":"22_CR2","unstructured":"Litmus tests for validation LISA-language Linux-kernel memory models. \n                      https:\/\/github.com\/paulmckrcu\/litmus\/tree\/master\/manual\/lwn573436"},{"key":"22_CR3","unstructured":"Programming Languages \u2014 C: ISO\/IEC 9899:2011 (2011). A non-final but recent version is available at \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/docs\/n1539.pdf"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-662-46681-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2015","unstructured":"Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353\u2013367. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-39799-8_9","volume-title":"Computer Aided Verification","author":"J Alglave","year":"2013","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of\u00a0concurrent\u00a0software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141\u2013157. Springer, Heidelberg (2013). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9"},{"key":"22_CR6","unstructured":"Alglave, J., Maranget, L.: Herd7 (in the diy tool suite) (2015). \n                      http:\/\/diy.inria.fr\/"},{"key":"22_CR7","doi-asserted-by":"publisher","unstructured":"Alglave, J., Maranget, L., McKenney, P.E., Parri, A., Stern, A.S.: Frightening small children and disconcerting grown-ups: concurrency in the Linux kernel. In: Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2018, Williamsburg, VA, USA, 24\u201328 March 2018, pp. 405\u2013418 (2018). \n                      https:\/\/doi.org\/10.1145\/3173162.3177156","DOI":"10.1145\/3173162.3177156"},{"issue":"2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2627752","volume":"36","author":"Jade Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR9","doi-asserted-by":"publisher","unstructured":"Batty, M., Donaldson, A.F., Wickerson, J.: Overhauling SC atomics in C11 and OpenCl. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 634\u2013648 (2016). \n                      https:\/\/doi.org\/10.1145\/2837614.2837637","DOI":"10.1145\/2837614.2837637"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-662-46669-8_12","volume-title":"Programming Languages and Systems","author":"M Batty","year":"2015","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 283\u2013307. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Proceeding POPL (2011)","DOI":"10.1145\/1926385.1926394"},{"key":"22_CR12","unstructured":"Becker, P. (ed.): Programming Languages \u2014 C++, iSO\/IEC 14882:2011 (2011). A non-final but recent version is available at \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2011\/n3242.pdf"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: Proceedings of PLDI, pp. 68\u201378. ACM, New York (2008)","DOI":"10.1145\/1379022.1375591"},{"key":"22_CR14","unstructured":"Boehm, H.J., Giroux, O., Vafeiadis, V.: P0668R2: Revising the C++ memory model. ISO WG21 paper (2018). \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p0668r2.html"},{"key":"22_CR15","doi-asserted-by":"publisher","unstructured":"Boehm, H., Demsky, B.: Outlawing ghosts: avoiding out-of-thin-air results. In: Proceedings of the Workshop on Memory Systems Performance and Correctness, MSPC 2014, Edinburgh, United Kingdom, 13 June 2014, pp. 7:1\u20137:6 (2014). \n                      https:\/\/doi.org\/10.1145\/2618128.2618134","DOI":"10.1145\/2618128.2618134"},{"key":"22_CR16","doi-asserted-by":"publisher","unstructured":"Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June 2017, pp. 467\u2013481 (2017). \n                      https:\/\/doi.org\/10.1145\/3062341.3062353","DOI":"10.1145\/3062341.3062353"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-319-52234-0_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P Cuoq","year":"2017","unstructured":"Cuoq, P., Runarvot, L., Cherepanov, A.: Detecting strict aliasing violations in the wild. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 14\u201333. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-52234-0_2"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of POPL (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Gadelha, M.Y.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength C model checker. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, 3\u20137 September 2018, pp. 888\u2013891 (2018)","DOI":"10.1145\/3238147.3240481"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-319-41528-4_24","volume-title":"Computer Aided Verification","author":"D Guth","year":"2016","unstructured":"Guth, D., Hathhorn, C., Saxena, M., Ro\u015fu, G.: RV-Match: practical semantics-based program analysis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016, Part I. LNCS, vol. 9779, pp. 447\u2013453. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41528-4_24"},{"key":"22_CR22","doi-asserted-by":"publisher","unstructured":"Hathhorn, C., Ellison, C., Rosu, G.: Defining the undefinedness of C. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15\u201317 June 2015, pp. 336\u2013345 (2015). \n                      https:\/\/doi.org\/10.1145\/2737924.2737979","DOI":"10.1145\/2737924.2737979"},{"key":"22_CR23","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for C\/C++ concurrency. PACMPL 2(POPL), 17:1\u201317:32 (2018). \n                      https:\/\/doi.org\/10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"22_CR24","unstructured":"Krebbers, R.: The C standard formalized in CoQ. Ph.D. thesis, Radboud University Nijmegen, December 2015"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker (competition contribution). In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"key":"22_CR26","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, 18\u201323 June 2017, pp. 618\u2013632 (2017). \n                      https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"22_CR27","unstructured":"Lee, J., Hur, C.K., Jung, R., Liu, Z., Regehr, J., Lopes, N.P.: Reconciling high-level optimizations and low-level code with twin memory allocation. In: Proceedings of the 2018 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2018, part of SPLASH 2018, Boston, MA, USA, 4\u20139 November 2018. ACM (2018)"},{"key":"22_CR28","unstructured":"Memarian, K., Gomes, V., Sewell, P.: Cerberus (2018). \n                      http:\/\/cerberus.cl.cam.ac.uk\/cerberus"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Memarian, K., et al.: Exploring C semantics and pointer provenance. In: Proceedings of 46th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2019. Proc. ACM Program. Lang. 3, POPL, Article 67","DOI":"10.1145\/3290380"},{"key":"22_CR30","unstructured":"Memarian, K., et al.: Exploring C semantics and pointer provenance. PACMPL 3(POPL), 67:1\u201367:32 (2019). \n                      https:\/\/dl.acm.org\/citation.cfm?id=3290380"},{"key":"22_CR31","doi-asserted-by":"crossref","unstructured":"Memarian, K., et al.: Into the depths of C: elaborating the de facto standards. In: PLDI 2016: 37th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation (Santa Barbara), June 2016. \n                      http:\/\/www.cl.cam.ac.uk\/users\/pes20\/cerberus\/pldi16.pdf\n                      \n                    . PLDI 2016 Distinguished Paper award","DOI":"10.1145\/2908080.2908081"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"22_CR33","doi-asserted-by":"publisher","unstructured":"Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C\/C++11 concurrency. In: Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, New York (2016). \n                      https:\/\/doi.org\/10.1145\/2983990.2983997","DOI":"10.1145\/2983990.2983997"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Norris, B., Demsky, B.: CDSchecker: checking concurrent data structures written with C\/C++ atomics. In: Proceedings of OOPSLA (2013)","DOI":"10.1145\/2509136.2509514"},{"key":"22_CR35","doi-asserted-by":"publisher","unstructured":"Ou, P., Demsky, B.: Towards understanding the costs of avoiding out-of-thin-air results. PACMPL 2(OOPSLA), 136:1\u2013136:29 (2018). \n                      https:\/\/doi.org\/10.1145\/3276506","DOI":"10.1145\/3276506"},{"key":"22_CR36","unstructured":"TrustInSoft: tis-interpreter (2017). \n                      http:\/\/trust-in-soft.com\/tis-interpreter\/\n                      \n                    . Accessed 11 Nov 2017"},{"key":"22_CR37","unstructured":"WG14: Defect report 260, September 2004. \n                      http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/dr_260.htm"},{"key":"22_CR38","doi-asserted-by":"publisher","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 190\u2013204. ACM, New York (2017). \n                      https:\/\/doi.org\/10.1145\/3009837.3009838","DOI":"10.1145\/3009837.3009838"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25540-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T11:04:53Z","timestamp":1562929493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25540-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255398","9783030255404"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25540-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}