{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:49:33Z","timestamp":1725814173905},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_25","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T04:25:44Z","timestamp":1418271944000},"page":"449-466","source":"Crossref","is-referenced-by-count":22,"title":["Effective Abstractions for Verification under Relaxed Memory Models"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Dan","sequence":"first","affiliation":[]},{"given":"Yuri","family":"Meshman","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Vechev","sequence":"additional","affiliation":[]},{"given":"Eran","family":"Yahav","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-642-33125-1_13","volume-title":"Static Analysis","author":"P.A. Abdulla","year":"2012","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Automatic fence insertion in integer programs via predicate abstraction. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 164\u2013180. Springer, Heidelberg (2012)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"508","DOI":"10.1007\/978-3-319-08867-9_33","volume-title":"Computer Aided Verification","author":"J. Alglave","year":"2014","unstructured":"Alglave, J., Kroening, D., Nimal, V., Poetzl, D.: Don\u2019t sit on the fence - a static analysis approach to automatic fence insertion. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 508\u2013524. Springer, Heidelberg (2014)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 512\u2013532. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-22110-1_9","volume-title":"Computer Aided Verification","author":"M.F. Atig","year":"2011","unstructured":"Atig, M.F., Bouajjani, A., Parlato, G.: Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 99\u2013115. Springer, Heidelberg (2011)"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 533\u2013553. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Burnim, J., Sen, K., Stergiou, C.: Testing concurrent programs on relaxed memory models. In: ISSTA 2011 (2011)","DOI":"10.1145\/2001420.2001436"},{"key":"25_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL 1977 (1977)","DOI":"10.1145\/512950.512973"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978 (1978)","DOI":"10.1145\/512760.512770"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Dan, A.M., Meshman, Y., Vechev, M., Yahav, E.: Predicate abstraction for relaxed memory models. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol.\u00a07935, pp. 84\u2013104. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-38856-9_7"},{"key":"25_CR11","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.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"2","key":"25_CR12","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s10270-012-0230-7","volume":"12","author":"B. Jeannet","year":"2013","unstructured":"Jeannet, B.: Relational interprocedural verification of concurrent programs. Software and System Modeling\u00a012(2), 285\u2013306 (2013)","journal-title":"Software and System Modeling"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"25_CR14","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD 2010 (2010)"},{"key":"25_CR15","doi-asserted-by":"crossref","unstructured":"Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: PLDI 2011 (2011)","DOI":"10.1145\/1993498.1993521"},{"issue":"9","key":"25_CR16","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput.\u00a028(9), 690\u2013691 (1979)","journal-title":"IEEE Trans. Comput."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Linden, A., Wolper, P.: An automata-based symbolic approach for verifying programs on relaxed memory models. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol.\u00a06349, pp. 212\u2013226. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16164-3_16"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Meshman, Y., Dan, A., Vechev, M., Yahav, E.: Synthesis of memory fences via refinement propagation. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 237\u2013252. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_15"},{"issue":"1","key":"25_CR19","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher Order Symbol. Comput.\u00a019(1), 31\u2013100 (2006)","journal-title":"Higher Order Symbol. Comput."},{"issue":"5","key":"25_CR20","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X. Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5), 26 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"25_CR21","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J. Sevc\u00edk","year":"2013","unstructured":"Sevc\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: Compcerttso: A verified compiler for relaxed-memory concurrency. J. ACM\u00a060(3), 22 (2013)","journal-title":"J. ACM"},{"issue":"2","key":"25_CR22","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D. Shasha","year":"1988","unstructured":"Shasha, D., Snir, M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst.\u00a010(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Sura, Z., Fang, X., Wong, C.-L., Midkiff, S.P., Lee, J., Padua, D.: Compiler techniques for high performance sequentially consistent java programs. In: PPoPP 2005 (2005)","DOI":"10.1145\/1065944.1065947"}],"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-662-46081-8_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T20:44:31Z","timestamp":1559076271000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}