{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T13:01:48Z","timestamp":1726059708316},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_5","type":"book-chapter","created":{"date-parts":[[2019,11,22]],"date-time":"2019-11-22T00:14:54Z","timestamp":1574381694000},"page":"83-100","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Program Logic for Dependence Analysis"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bubel","sequence":"first","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]},{"given":"Asmae","family":"Heydari Tabar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification \u2013 The KeY Book: From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification \u2013 The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"4","key":"5_CR2","doi-asserted-by":"publisher","first-page":"987","DOI":"10.1007\/s10270-015-0476-y","volume":"15","author":"E Albert","year":"2016","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., D\u00edez, G.R.: A formal verification framework for static analysis\u2013as well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. Softw. Syst. Model. 15(4), 987\u20131012 (2016)","journal-title":"Softw. Syst. Model."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Allen, F.E., Burke, M.G., Cytron, R., Ferrante, J., Hsieh, W.C.: A framework for determining useful parallelism. In: Lenfant, J. (ed.) Proceedings of the 2nd International Conference on Supercomputing, pp. 207\u2013215. ACM (1988)","DOI":"10.1145\/55364.55385"},{"issue":"5","key":"5_CR4","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1023\/A:1007588710878","volume":"28","author":"W Amme","year":"2000","unstructured":"Amme, W., Braun, P., Thomasset, F., Zehendner, E.: Data dependence analysis of assembly code. Int. J. Parallel Program. 28(5), 431\u2013467 (2000)","journal-title":"Int. J. Parallel Program."},{"issue":"2","key":"5_CR5","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00128174","volume":"2","author":"U Banerjee","year":"1988","unstructured":"Banerjee, U.: An introduction to a formal theory of dependence analysis. J. Supercomput. 2(2), 133\u2013149 (1988)","journal-title":"J. Supercomput."},{"key":"5_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). \nwww.SMT-LIB.org"},{"key":"5_CR7","unstructured":"Cytron, R., Ferrante, J.: What\u2019s in a name? -or- the value of renaming for parallelism detection and storage allocation. In: International Conference on Parallel Processing, pp. 19\u201327. Pennsylvania State University Press (1987)"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/BF01407931","volume":"20","author":"P Feautrier","year":"1991","unstructured":"Feautrier, P.: Dataflow analysis of array and scalar references. Int. J. Parallel Program. 20(1), 23\u201353 (1991)","journal-title":"Int. J. Parallel Program."},{"issue":"3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Garcia, S., Jeon, D., Louie, C.M., Taylor, M.B.: Kremlin: rethinking and rebooting gprof for the multicore age. In: Hall, M.W., Padua, D.A. (eds.) 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 458\u2013469. ACM (2011)","DOI":"10.1145\/1993498.1993553"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/3-540-63166-6_10"},{"issue":"10","key":"5_CR12","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). \nhttps:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Huda, Z.U., Atre, R., Jannesari, A., Wolf, F.: Automatic parallel pattern detection in the algorithm structure design space. In: 30th IEEE International Parallel and Distributed Processing Symposium, pp. 43\u201352. IEEE Computer Society (2016)","DOI":"10.1109\/IPDPS.2016.60"},{"issue":"7","key":"5_CR14","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). \nhttps:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Li, Z., Jannesari, A., Wolf, F.: An efficient data-dependence profiler for sequential and parallel programs. In: IEEE International Parallel and Distributed Processing Symposium, pp. 484\u2013493. IEEE Computer Society (2015)","DOI":"10.1109\/IPDPS.2015.41"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Liu, W., et al.: POSH: a TLS compiler that exploits program structure. In: Torrellas, J., Chatterjee, S. (eds.) ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP, pp. 158\u2013167. ACM (2006)","DOI":"10.1145\/1122971.1122997"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/3-540-57502-2_63","volume-title":"Languages and Compilers for Parallel Computing","author":"D Maydan","year":"1993","unstructured":"Maydan, D., Amarsinghe, S., Lam, M.: Data dependence and data-flow analysis of arrays. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1992. LNCS, vol. 757, pp. 434\u2013448. Springer, Heidelberg (1993). \nhttps:\/\/doi.org\/10.1007\/3-540-57502-2_63"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"von Praun, C., Bordawekar, R., Cascaval, C.: Modeling optimistic concurrency using quantitative dependence analysis. In: Chatterjee, S., Scott, M.L. (eds.) 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP, pp. 185\u2013196. ACM (2008)","DOI":"10.1145\/1345206.1345234"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Martin, J.L. (ed.) Proceedings Supercomputing 1991, pp. 4\u201313. ACM (1991)","DOI":"10.1145\/125826.125848"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/3-540-57659-2_31","volume-title":"Languages and Compilers for Parallel Computing","author":"W Pugh","year":"1994","unstructured":"Pugh, W., Wonnacott, D.: An exact method for analysis of value-based array data dependences. In: Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1993. LNCS, vol. 768, pp. 546\u2013566. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/3-540-57659-2_31"},{"issue":"4","key":"5_CR21","doi-asserted-by":"publisher","first-page":"1248","DOI":"10.1145\/183432.183525","volume":"16","author":"W Pugh","year":"1994","unstructured":"Pugh, W., Wonnacott, D.: Static analysis of upper and lower bounds on dependences and parallelism. ACM Trans. Program. Lang. Syst. 16(4), 1248\u20131278 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, D., Yen, L., Hill, M.D., Sankaralingam, K.: Implementing signatures for transactional memory. In: 40th Annual IEEE\/ACM International Symposium on Microarchitecture, pp. 123\u2013133. IEEE Computer Society (2007)","DOI":"10.1109\/MICRO.2007.24"},{"issue":"6","key":"5_CR23","first-page":"280","volume":"56","author":"G Snelting","year":"2014","unstructured":"Snelting, G., et al.: Checking probabilistic noninterference using JOANA. it - Inf. Technol. 56(6), 280\u2013287 (2014)","journal-title":"it - Inf. Technol."},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Wasser, N., Bubel, R., H\u00e4hnle, R.: Abstract interpretation. In: Ahrendt et al. [1], chap. 6, pp. 167\u2013189","DOI":"10.1007\/978-3-319-49812-6_6"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-89740-8_16","volume-title":"Languages and Compilers for Parallel Computing","author":"P Wu","year":"2008","unstructured":"Wu, P., Kejariwal, A., Ca\u015fcaval, C.: Compiler-driven dependence profiling to guide program parallelization. In: Amaral, J.N. (ed.) LCPC 2008. LNCS, vol. 5335, pp. 232\u2013248. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-89740-8_16"},{"key":"5_CR26","unstructured":"Yuki, T., Pouchet, L.N.: Polybench\/c 4.1 (2015). \nhttp:\/\/web.cse.ohio-state.edu\/~pouchet.2\/software\/polybench\/"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Zhang, X., Navabi, A., Jagannathan, S.: Alchemist: a transparent dependence distance profiling infrastructure. In: The Seventh International Symposium on Code Generation and Optimization, pp. 47\u201358. IEEE Computer Society (2009)","DOI":"10.1109\/CGO.2009.15"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,22]],"date-time":"2019-11-22T00:17:39Z","timestamp":1574381859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_5","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":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","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":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}