{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T21:08:25Z","timestamp":1725916105154},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_4","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T14:42:30Z","timestamp":1510411350000},"page":"51-66","source":"Crossref","is-referenced-by-count":1,"title":["A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models"],"prefix":"10.1007","author":[{"given":"Tatsuya","family":"Abe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"4_CR1","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). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_28"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-662-54580-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2017","unstructured":"Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 56\u201374. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_4"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-41540-6_8","volume-title":"Computer Aided Verification","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134\u2013156. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_8"},{"key":"4_CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.2197\/ipsjjip.25.244","volume":"25","author":"T Abe","year":"2017","unstructured":"Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. Journal of Information Processing 25, 244\u2013255 (2017)","journal-title":"Journal of Information Processing"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. International Journal on Software Tools for Technology Transfer 19(5) (2017). https:\/\/bitbucket.org\/abet\/mcspin\/","DOI":"10.1007\/s10009-016-0429-y"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Abe, T., Ugawa, T., Maeda, T.: Reordering control approaches to state explosion in model checking with memory consistency models. In: Proc. of VSTTE (2017)","DOI":"10.1007\/978-3-319-72308-2_11"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-47677-3_8","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"T Abe","year":"2016","unstructured":"Abe, T., Ugawa, T., Maeda, T., Matsumoto, K.: Reducing state explosion for software model checking with relaxed memory consistency models. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 118\u2013135. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_8"},{"issue":"12","key":"4_CR8","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer 29(12), 66\u201376 (1996)","journal-title":"Computer"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems 36(2) (2014). http:\/\/diy.inria.fr\/herd\/","DOI":"10.1145\/2627752"},{"issue":"6","key":"4_CR10","doi-asserted-by":"crossref","first-page":"1056","DOI":"10.1109\/TPDS.2010.172","volume":"22","author":"AA Aravind","year":"2011","unstructured":"Aravind, A.A.: Yet another simple solution for the concurrent programming control problem. IEEE Transactions on Parallel and Distributed Systems 22(6), 1056\u20131063 (2011)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S Blom","year":"2010","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354\u2013359. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_31"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W.: Cooperating sequential processes. In: Programming Languages: NATO Advanced Study Institute, pp. 43\u2013112. Academic Press (1968)","DOI":"10.1007\/978-1-4757-3472-0_2"},{"key":"4_CR13","unstructured":"Edelkamp, S., Lafuente, A.L.: HSF-SPIN User Manual (2006)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57\u201379. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45139-0_5"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-642-00431-5_5","volume-title":"Model Checking and Artificial Intelligence","author":"S Edelkamp","year":"2009","unstructured":"Edelkamp, S., Schuppan, V., Bo\u0161na\u010dki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS (LNAI), vol. 5348, pp. 65\u201389. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00431-5_5"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Fischer, B., Inverso, O., Parlato, G.: CSeq: A concurrency pre-processor for sequential C verification tools. In: Proc. of ASE, pp. 710\u2013713 (2013)","DOI":"10.1109\/ASE.2013.6693139"},{"key":"4_CR17","unstructured":"Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley (2003)"},{"issue":"8","key":"4_CR18","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of Dijkstra\u2019s concurrent programming problem. Comm. ACM 17(8), 453\u2013455 (1974)","journal-title":"Comm. ACM"},{"key":"4_CR19","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"9","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 9, 690\u2013691 (1979)","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"4_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L Lamport","year":"1987","unstructured":"Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1\u201311 (1987)","journal-title":"ACM Transactions on Computer Systems"},{"key":"4_CR21","unstructured":"Leijen, D., Palamarchuk, A.: The IntMap module. https:\/\/hackage.haskell.org\/package\/containers-0.5.10.2\/docs\/Data-IntMap.html"},{"key":"4_CR22","unstructured":"McCloskey, B., Bacon, D.F., Cheng, P., Grove, D.: Staccato: A parallel and concurrent real-time compacting garbage collector for multiprocessors. Research Report RC24504, IBM (2008)"},{"key":"4_CR23","unstructured":"Nidhugg: Nidhugg Manual, Version 0.2 (2016). https:\/\/github.com\/nidhugg"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. Technical Report UCAM-CL-TR-745, Computer Laboratory, University of Cambridge (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"issue":"3","key":"4_CR25","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"GL Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115\u2013116 (1981)","journal-title":"Information Processing Letters"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Pizlo, F., Petrank, E., Steensgaard, B.: A study of concurrent real-time garbage collectors. Proc. of PLDI, pp. 33\u201344 (2008)","DOI":"10.1145\/1375581.1375587"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/3-540-48119-2_13","volume-title":"FM\u201999 \u2014 Formal Methods","author":"F Reffe","year":"1999","unstructured":"Reffe, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 195\u2013211. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_13"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proc. of PLDI, pp. 175\u2013186 (2011)","DOI":"10.1145\/1993498.1993520"},{"key":"4_CR29","unstructured":"Still, V.: LLVM transformations for model checking. Master\u2019s thesis, Masaryk University (2016)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-29817-7_13","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"V \u0160till","year":"2016","unstructured":"\u0160till, V., Ro\u010dkai, P., Barnat, J.: Weak memory models as LLVM-to-LLVM transformations. In: Kofro\u0148, J., Vojnar, T. (eds.) MEMICS 2015. LNCS, vol. 9548, pp. 144\u2013155. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29817-7_13"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Tomasco, E., Truc Nguyen Lam, O.I., Fischer, B., Torre, S.L., Parlato, G.: Lazy sequentialization for TSO and PSO via shared memory abstractions. In: Proc. of FMCAD, pp. 193\u2013200 (2016)","DOI":"10.1109\/FMCAD.2016.7886679"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-46750-4_1","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"O Travkin","year":"2016","unstructured":"Travkin, O., Wehrheim, H.: Verification of concurrent programs on weak memory models. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 3\u201324. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_1"},{"key":"4_CR33","doi-asserted-by":"crossref","unstructured":"Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: Proc. of OOPSLA, pp. 691\u2013707 (2014)","DOI":"10.1145\/2660193.2660243"},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for C11 concurrency. In: Proc. of OOPSLA, pp. 867\u2013884 (2013)","DOI":"10.1145\/2509136.2509532"},{"key":"4_CR35","unstructured":"van der Berg, F.: Model checking LLVM IR using LTSmin: Using relaxed memory model semantics. Master\u2019s thesis. University of Twente (2013)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70389-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T01:29:20Z","timestamp":1570325360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}