{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:41:09Z","timestamp":1725536469281},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032363"},{"type":"electronic","value":"9783642032370"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03237-0_6","type":"book-chapter","created":{"date-parts":[[2009,8,3]],"date-time":"2009-08-03T01:24:37Z","timestamp":1249262677000},"page":"52-68","source":"Crossref","is-referenced-by-count":8,"title":["Automatic Parallelization and Optimization of Programs by Proof Rewriting"],"prefix":"10.1007","author":[{"given":"Cl\u00e9ment","family":"Hurlin","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Proof trees of the examples, additional examples, and open source implementation, http:\/\/www-sop.inria.fr\/everest\/Clement.Hurlin\/eterlou\/eterlou.shtml"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Nicolau, A.: Optimal loop parallelization. ACM SIGPLAN Notices\u00a023(7) (1988)","DOI":"10.1145\/960116.54021"},{"key":"6_CR3","volume-title":"International Conference on Supercomputing","author":"P. Artigas","year":"2000","unstructured":"Artigas, P., Gupta, M., Midkiff, S., Moreira, J.: Automatic loop transformations and parallelization for Java. In: International Conference on Supercomputing. ACM Press, New York (2000)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-540-73449-9_5","volume-title":"Term Rewriting and Applications","author":"E. Balland","year":"2007","unstructured":"Balland, E., Brauner, P., Kopetz, R., Moreau, P.-E., Reilles, A.: Tom: Piggybacking rewriting on Java. In: Baader, F. (ed.) RTA 2007. LNCS, vol.\u00a04533, pp. 36\u201347. Springer, Heidelberg (2007)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 301\u2013317. Springer, Heidelberg (2006)"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111. Springer, Heidelberg (2006)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Bik, A., Gannon, D.: Automatically exploiting implicit parallelism in Java. Concurrency: Practice and Experience \u00a09 (1997)","DOI":"10.1002\/(SICI)1096-9128(199706)9:6<579::AID-CPE309>3.0.CO;2-G"},{"key":"6_CR10","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Mathematical Foundations of Programming Semantics","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. In: Mathematical Foundations of Programming Semantics. Electronic Notes in Theoretical Computer Science, vol.\u00a0155. Elsevier, Amsterdam (2005)"},{"key":"6_CR11","volume-title":"ACM Conference on Object-Oriented Programming Systems, Languages, and Applications","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications. ACM Press, New York (2002)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Static Analysis Symposium","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694. Springer, Heidelberg (2003)"},{"key":"6_CR13","volume-title":"Principles of Programming Languages","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., OHearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Shao, Z., Pierce, B.C. (eds.) Principles of Programming Languages. ACM Press, New York (to appear, 2009)"},{"key":"6_CR14","volume-title":"Principles of Programming Languages","author":"W. Chin","year":"2008","unstructured":"Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: Necula, G.C., Wadler, P. (eds.) Principles of Programming Languages. ACM Press, New York (2008)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-78791-4_19","volume-title":"Compiler Construction","author":"D. Cunningham","year":"2008","unstructured":"Cunningham, D., Gudka, K., Eisenbach, S.: Keep off the grass: Locking the right path for atomicity. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 276\u2013290. Springer, Heidelberg (2008)"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11691372_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Distefano","year":"2006","unstructured":"Distefano, D., O\u2019Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 287\u2013302. Springer, Heidelberg (2006)"},{"key":"6_CR17","volume-title":"ACM Conference on Object-Oriented Programming Systems, Languages, and Applications","author":"D. DiStefano","year":"2008","unstructured":"DiStefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, vol.\u00a043. ACM Press, New York (2008)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Ergin, O., Balkan, D., Ponomarev, D., Ghose, K.: Early register deallocation mechanisms using checkpointed register files. IEEE Computer\u00a055 (2006)","DOI":"10.1109\/TC.2006.145"},{"key":"6_CR19","volume-title":"International Conference on Compiler Construction","author":"R. Ghiya","year":"1998","unstructured":"Ghiya, R., Hendren, L.J., Zhu, Y.: Detecting parallelism in c programs with recursive data structures. In: Koskimies, K. (ed.) CC 1998, vol.\u00a01383. Springer, Heidelberg (1998)"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Gupta, R., Pande, S., Psarris, K., Sarkar, V.: Compilation techniques for parallel systems. Parallel Computing\u00a025(13) (1999)","DOI":"10.1016\/S0167-8191(99)00086-1"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-89330-1_13","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2008","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java\u2019s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 171\u2013187. Springer, Heidelberg (2008)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C. Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. In: Meseguer, J., Rosu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Hendren, L.J., Nicolau, A.: Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems\u00a01 (1990)","DOI":"10.1109\/71.80123"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Hurlin, C.: Automatic parallelization and optimization of programs by proof rewriting. Technical Report 6806, INRIA. Initial version: January 2009, revised version: April 2009","DOI":"10.1007\/978-3-642-03237-0_6"},{"key":"6_CR26","unstructured":"Jacobs, B., Piessens, F.: The verifast program verifier. Technical Report CW520, Katholieke Universiteit Leuven (2008)"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Lamport, L.: The parallel execution of do loops. Communications of the ACM\u00a017(2) (1974)","DOI":"10.1145\/360827.360844"},{"key":"6_CR28","volume-title":"Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Principles of Programming Languages. ACM Press, New York (2006)"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. ACM SIGPLAN Notices\u00a035(5) (2000)","DOI":"10.1145\/358438.349314"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science\u00a0375(1-3) (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"6_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 1. Springer, Heidelberg (2001) (invited paper)"},{"key":"6_CR32","unstructured":"Parkinson, M.: Local Reasoning for Java. Ph.D thesis, University of Cambridge (2005)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Raza, M., Calcagno, C., Gardner, P.: Automatic parallelization with separation logic. In: European Symposium on Programming (to appear, 2009)","DOI":"10.1007\/978-3-642-00590-9_25"},{"key":"6_CR34","volume-title":"Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science. IEEE Press, Los Alamitos (2002)"},{"key":"6_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, p. 63. Springer, Heidelberg (2002)"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Xue, C., Shao, Z., Sha, E.-M.: Maximize parallelism minimize overhead for nested loops via loop striping. Journal of VLSI Signal Processing Systems\u00a047(2) (2007)","DOI":"10.1007\/s11265-006-0034-5"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03237-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T16:33:28Z","timestamp":1558456408000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03237-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032363","9783642032370"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03237-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}