{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T08:38:16Z","timestamp":1743064696433,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642177958"},{"type":"electronic","value":"9783642177965"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-17796-5_2","type":"book-chapter","created":{"date-parts":[[2011,1,11]],"date-time":"2011-01-11T12:08:27Z","timestamp":1294747707000},"page":"28-43","source":"Crossref","is-referenced-by-count":1,"title":["Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra"],"prefix":"10.1007","author":[{"given":"Claude","family":"Bolduc","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"B\u00e9chir","family":"Ktari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. of the 36th ACM symp. on Theory of computing, New York, USA, pp. 202\u2013211 (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bolduc, C., Ktari, B.: Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra (extended version). Technical Report DIUL-RR-1001, Universit\u00e9 Laval, QC, Canada (2010)","DOI":"10.1007\/978-3-642-17796-5_2"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-04639-1_4","volume-title":"Relations and Kleene Algebra in Computer Science","author":"C. Bolduc","year":"2009","unstructured":"Bolduc, C., Ktari, B.: Visibly pushdown Kleene algebra and its use in interprocedural analysis of (mutually) recursive programs. In: Berghammer, R., Jaoua, A.M., M\u00f6ller, B. (eds.) RelMiCS 2009. LNCS, vol.\u00a05827, pp. 44\u201358. Springer, Heidelberg (2009)"},{"issue":"2","key":"2_CR4","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390 (1994)","journal-title":"Information and Computation"},{"key":"2_CR5","unstructured":"Kozen, D.: Efficient code certification. Technical Report 98-1661, Cornell University, Ithaca, USA (1998)"},{"issue":"3","key":"2_CR6","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. Transactions on Programming Languages and Systems\u00a019(3), 427\u2013443 (1997)","journal-title":"Transactions on Programming Languages and Systems"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Nonlocal flow of control and Kleene algebra with tests. In: Proc. 23rd IEEE Symp. Logic in Computer Science, pp. 105\u2013117 (June 2008)","DOI":"10.1109\/LICS.2008.32"},{"key":"2_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1007\/3-540-44957-4_38","volume-title":"Computational Logic - CL 2000","author":"D. Kozen","year":"2000","unstructured":"Kozen, D., Patron, M.C.: Certification of compiler optimizations using Kleene algebra with tests. In: Palamidessi, C., et al. (eds.) CL 2000. LNCS (LNAI), vol.\u00a01861, pp. 568\u2013582. Springer, Heidelberg (2000)"},{"issue":"3","key":"2_CR9","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Transactions on Programming Languages and Systems\u00a021(3), 527\u2013568 (1999)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proc. of the 24th ACM SIGPLAN-SIGACT symp. on Principles of programming languages, New York, USA, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10721959_3","volume-title":"Automated Deduction - CADE-17","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C., Lee, P.: Proof generation in the Touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 25\u201344. Springer, Heidelberg (2000)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Zaks, A., Pnueli, A.: Program analysis for compiler validation. In: Proc. of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, New York, USA, pp. 1\u20137 (2008)","DOI":"10.1145\/1512475.1512477"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17796-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T15:16:32Z","timestamp":1559920592000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17796-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642177958","9783642177965"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17796-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}