{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:51:01Z","timestamp":1725511861738},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_15","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T02:37:44Z","timestamp":1210127864000},"page":"200-217","source":"Crossref","is-referenced-by-count":3,"title":["Automatic Certification of Java Source Code in Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Mauricio","family":"Alba-Castro","sequence":"first","affiliation":[]},{"given":"Mar\u00eda","family":"Alpuente","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-540-32275-7_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E. Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 380\u2013397. Springer, Heidelberg (2005)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instuctions for proof-carrying code. In: POPL, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"issue":"3","key":"15_CR3","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci.\u00a0364(3), 273\u2013291 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","author":"L. Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"issue":"3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: Proc. of Sixth ACM Symp. on Principles of Programming Languages, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"15_CR10","unstructured":"Farzan, A., Chen, F., Meseguer, J., Rosu, G.: JavaRL: The rewriting logic semantics of Java (2007), http:\/\/fsl.cs.uiuc.edu\/index.php\/Rewriting_Logic_Semantics_of_Java"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Rosu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 501\u2013505. Springer, Heidelberg (2004)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-540-27815-3_14","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Meseguer, J., Rosu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 132\u2013147. Springer, Heidelberg (2004)"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/978-3-540-32033-3_29","volume-title":"Term Rewriting and Applications","author":"A.P. Felty","year":"2005","unstructured":"Felty, A.P.: A tutorial example of the semantic approach to foundational proof-carrying code. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 394\u2013406. Springer, Heidelberg (2005)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"issue":"3","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G. Leavens","year":"2006","unstructured":"Leavens, G., Baker, A., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci.\u00a096(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"15_CR17","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theor. Comput. Sci.\u00a0373(3), 213\u2013237 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT Annual Symposium on Principles of Programming Languages POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Annual Symposium on Principles of Programming Languages POPL 1997, Paris, France, pp. 106\u2013119. ACM Press, New York, NY, USA (1997)"},{"key":"15_CR19","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/238721.238781","volume-title":"Proc. of the second USENIX symposium on Operating systems design and implementation OSDI 1996","author":"G.C. Necula","year":"1996","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run time checking. In: Proc. of the second USENIX symposium on Operating systems design and implementation OSDI 1996, pp. 229\u2013243. ACM Press, New York (1996)"},{"key":"15_CR20","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"key":"15_CR21","first-page":"333","volume-title":"3rd Int\u2019ll Conf. on Theoretical Computer Science (TCS 2004)","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T., Klein, G., Nanz, S.: Prototyping proof carrying code. In: L\u00e9vy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) 3rd Int\u2019ll Conf. on Theoretical Computer Science (TCS 2004), pp. 333\u2013348. Kluwer, Dordrecht (2004)"},{"key":"15_CR22","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/888251.888276","volume-title":"Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declarative programming PPDP","author":"D. Wu","year":"2003","unstructured":"Wu, D., Appel, A., Stump, A.: Foundational proof checkers with small witnesses. In: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declarative programming PPDP, pp. 264\u2013274. ACM Press, New York (2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:28:37Z","timestamp":1619508517000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_15","relation":{},"subject":[]}}