{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,14]],"date-time":"2023-01-14T12:50:54Z","timestamp":1673700654589},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2006,11]]},"abstract":"<jats:p>The SSP is a hardware implementation of a subset of the JVM for use in high-consequence embedded applications. In this context, a majority of the activities belonging to class loading, as it is defined in the specification of the JVM, can be performed statically. Static class loading has the net result of dramatically simplifying the design of the SSP, as well as increasing its performance. Because of the high consequence nature of its applications, strong evidence must be provided that all aspects of the SSP have been implemented correctly. This includes the class loader. This article explores the possibility of formally verifying a class loader for the SSP implemented in the strategic programming language TL. Specifically, an implementation of the core activities of an abstract class loader is presented and its verification in ACL2 is considered.<\/jats:p>","DOI":"10.1145\/1196636.1196639","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"773-818","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A transformational perspective into the core of an abstract class loader for the SSP"],"prefix":"10.1145","volume":"5","author":[{"given":"Victor L.","family":"Winter","sequence":"first","affiliation":[{"name":"University of Nebraska at Omaha, Omaha, Nebraska"}]},{"given":"Jason","family":"Beranek","sequence":"additional","affiliation":[{"name":"University of Nebraska at Omaha, Omaha, Nebraska"}]},{"given":"Fares","family":"Fraij","sequence":"additional","affiliation":[{"name":"University of Texas at El Paso, El Paso, Texas"}]},{"given":"Steve","family":"Roach","sequence":"additional","affiliation":[{"name":"University of Texas at El Paso, El Paso, Texas"}]},{"given":"Greg","family":"Wickstrom","sequence":"additional","affiliation":[{"name":"Sandia National Laboratories, Albuquerque, New Mexico"}]}],"member":"320","published-online":{"date-parts":[[2006,11]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Bergstra J. A. 1989. Algebraic Specification. ACM Press New York.]]   Bergstra J. A. 1989. Algebraic Specification. ACM Press New York.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Borovansk\u00fd P. Kirchner C. Kirchner H. Moreau P.-E. and Ringeissen C. 1998. An overview of elan. Electr. Notes Theor. Comput. Sci. 15.]]  Borovansk\u00fd P. Kirchner C. Kirchner H. Moreau P.-E. and Ringeissen C. 1998. An overview of elan. Electr. Notes Theor. Comput. Sci. 15.]]","DOI":"10.1016\/S1571-0661(05)80011-8"},{"key":"e_1_2_1_3_1","unstructured":"Boyer R. S. and Moore J. S. 1988. A Computational Logic Handbook. Academic Press New York.]]   Boyer R. S. and Moore J. S. 1988. A Computational Logic Handbook. Academic Press New York.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227603"},{"key":"e_1_2_1_5_1","volume-title":"Research Report RR-3818, INRIA (Dec.).]]","author":"Cirstea H.","year":"1999","unstructured":"Cirstea , H. and Kirchner , C . 1999 . An Introduction to the Rewriting Calculus . Research Report RR-3818, INRIA (Dec.).]] Cirstea, H. and Kirchner, C. 1999. An Introduction to the Rewriting Calculus. Research Report RR-3818, INRIA (Dec.).]]"},{"key":"e_1_2_1_6_1","unstructured":"HATS. http:\/\/faculty.ist.unomaha.edu\/winter\/hats-uno\/hatsweb\/index.html.]]  HATS. http:\/\/faculty.ist.unomaha.edu\/winter\/hats-uno\/hatsweb\/index.html.]]"},{"key":"e_1_2_1_7_1","volume-title":"Eds","author":"Kaufmann M.","year":"2000","unstructured":"Kaufmann , M. , Manolios , P. , and Moore , J. S. , Eds . 2000 a. Computer-Aided Reasoning: An Approach . Kluwer Academic Publishers , Boston, MA.]] Kaufmann, M., Manolios, P., and Moore, J. S., Eds. 2000a. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston, MA.]]"},{"key":"e_1_2_1_8_1","volume-title":"Eds","author":"Kaufmann M.","year":"2000","unstructured":"Kaufmann , M. , Manolios , P. , and Moore , J. S. , Eds . 2000 b. Computer-Aided Reasoning: Case Studies . Kluwer Academic Publishers , Boston, MA.]] Kaufmann, M., Manolios, P., and Moore, J. S., Eds. 2000b. Computer-Aided Reasoning: Case Studies. Kluwer Academic Publishers, Boston, MA.]]"},{"key":"e_1_2_1_9_1","volume-title":"Eds","author":"Lindholm T.","year":"1999","unstructured":"Lindholm , T. and Yellin , F. , Eds . 1999 . The Java Virtual Machine 2nd ed. Addison-Wesley , Reading, MA.]] Lindholm, T. and Yellin, F., Eds. 1999. The Java Virtual Machine 2nd ed. Addison-Wesley, Reading, MA.]]"},{"key":"e_1_2_1_10_1","volume-title":"IVME '03: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators. ACM Press","author":"Liu H.","unstructured":"Liu , H. and Moore , J. S . 2003. Executable jvm model for analytical reasoning: A study . In IVME '03: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators. ACM Press , New York. 15--23.]] 10.1145\/858570.858572 Liu, H. and Moore, J. S. 2003. Executable jvm model for analytical reasoning: A study. In IVME '03: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators. ACM Press, New York. 15--23.]] 10.1145\/858570.858572"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Liu H. and Moore J. S. 2004. Java program verification via a jvm deep embedding in acl2.]]  Liu H. and Moore J. S. 2004. Java program verification via a jvm deep embedding in acl2.]]","DOI":"10.1007\/978-3-540-30142-4_14"},{"key":"e_1_2_1_12_1","volume-title":"HASE 2004: The 5th IEEE International Symposium on High Assurance Systems Engineering.]]","author":"McCoy J. A.","year":"2000","unstructured":"McCoy , J. A. 2000 . An embedded system for safe, secure and reliable execution of high consequence software . In HASE 2004: The 5th IEEE International Symposium on High Assurance Systems Engineering.]] McCoy, J. A. 2000. An embedded system for safe, secure and reliable execution of high consequence software. In HASE 2004: The 5th IEEE International Symposium on High Assurance Systems Engineering.]]"},{"key":"e_1_2_1_13_1","volume-title":"1996. Piton: A Mechanically Verified Assembly-Level Language (Automated Reasoning Series)","author":"Moore J. S.","unstructured":"Moore , J. S. , Eds. 1996. Piton: A Mechanically Verified Assembly-Level Language (Automated Reasoning Series) . Kluwer Academic Publishers . Boston, MA.]] Moore, J. S., Eds. 1996. Piton: A Mechanically Verified Assembly-Level Language (Automated Reasoning Series). Kluwer Academic Publishers. Boston, MA.]]"},{"key":"e_1_2_1_14_1","volume-title":"Correct System Design, Recent Insight and Advances (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel)","author":"Moore J. S.","unstructured":"Moore , J. S. 1999. Proving theorems about Java-like byte code . In Correct System Design, Recent Insight and Advances (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel) , Springer-Verlag , New York . 139--162.]] Moore, J. S. 1999. Proving theorems about Java-like byte code. In Correct System Design, Recent Insight and Advances (to Hans Langmaack on the Occasion of his Retirement from his Professorship at the University of Kiel), Springer-Verlag, New York. 139--162.]]"},{"key":"e_1_2_1_15_1","volume-title":"Models, Algebras and Logic of Engineering Software","author":"Moore J. S.","unstructured":"Moore , J. S. 2003. Proving theorems about Java and the JVM with ACL2 . In Models, Algebras and Logic of Engineering Software . IOS Press , Amsterdam . 227--290.]] Moore, J. S. 2003. Proving theorems about Java and the JVM with ACL2. In Models, Algebras and Logic of Engineering Software. IOS Press, Amsterdam. 227--290.]]"},{"key":"e_1_2_1_16_1","volume-title":"Java Virtual Machine Research and Technology Symposium. 91--104","author":"Moore J. S.","unstructured":"Moore , J. S. and Porter , G . 2001. An executable formal java virtual machine thread model . In Java Virtual Machine Research and Technology Symposium. 91--104 .]] Moore, J. S. and Porter, G. 2001. An executable formal java virtual machine thread model. In Java Virtual Machine Research and Technology Symposium. 91--104.]]"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/941566.941568"},{"key":"e_1_2_1_18_1","volume-title":"Inside the Java Virtual Machine","author":"Venners B.","unstructured":"Venners , B. 1998. Inside the Java Virtual Machine . McGraw-Hill , New York .]] Venners, B. 1998. Inside the Java Virtual Machine. McGraw-Hill, New York.]]"},{"key":"e_1_2_1_19_1","volume-title":"RtA '99: Proceedings of the 10th International Conference on Rewriting Techniques and Applications","author":"Visser E.","year":"1999","unstructured":"Visser , E. 1999 . Strategic pattern matching . In RtA '99: Proceedings of the 10th International Conference on Rewriting Techniques and Applications . London. Springer-Verlag, New York. 30--44.]] Visser, E. 1999. Strategic pattern matching. In RtA '99: Proceedings of the 10th International Conference on Rewriting Techniques and Applications. London. Springer-Verlag, New York. 30--44.]]"},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1016\/S1571-0661(04)00298-1","article-title":"Scoped dynamic rewrite rules","volume":"59","author":"Visser E.","year":"2001","unstructured":"Visser , E. 2001 . Scoped dynamic rewrite rules . Electronic Notes in Theoretical Computer Science , 59 , 4 .]] Visser, E. 2001. Scoped dynamic rewrite rules. Electronic Notes in Theoretical Computer Science, 59, 4.]]","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP'98)","author":"Visser E.","unstructured":"Visser , E. , Benaissa , Z. e. A. , and Tolmach , A . 1998. Building program optimizers with rewriting strategies . In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP'98) . 13--26.]] 10.1145\/289423.289425 Visser, E., Benaissa, Z. e. A., and Tolmach, A. 1998. Building program optimizers with rewriting strategies. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (ICFP'98). 13--26.]] 10.1145\/289423.289425"},{"key":"e_1_2_1_22_1","volume-title":"HASE 2004: The 8th IEEE International Symposium on High Assurance Systems Engineering.]]","author":"Wickstrom G. L.","unstructured":"Wickstrom , G. L. , Davis , J. , Morrison , S. E. , Roach , S. , and Winter , V. L . 2004. The ssp: An example of high-assurance system engineering . In HASE 2004: The 8th IEEE International Symposium on High Assurance Systems Engineering.]] Wickstrom, G. L., Davis, J., Morrison, S. E., Roach, S., and Winter, V. L. 2004. The ssp: An example of high-assurance system engineering. In HASE 2004: The 8th IEEE International Symposium on High Assurance Systems Engineering.]]"},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Winter V. 2004b. Strategy construction in the higher-order framework of TL. Electronic Notes in Theoretical Computer Science (ENTCS) 124.]]  Winter V. 2004b. Strategy construction in the higher-order framework of TL. Electronic Notes in Theoretical Computer Science (ENTCS) 124.]]","DOI":"10.1016\/j.entcs.2004.07.020"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.03.006"},{"key":"e_1_2_1_26_1","first-page":"47","article-title":"Transformation-oriented programming: A development methodology for high assurance software. In Advances in Computers: Highly Dependable Software, M. Zelkowitz","volume":"58","author":"Winter V. L.","year":"2003","unstructured":"Winter , V. L. , Roach , S. , and Wickstrom , G. 2003 . Transformation-oriented programming: A development methodology for high assurance software. In Advances in Computers: Highly Dependable Software, M. Zelkowitz , Ed. vol. 58. 47 -- 116 .]] Winter, V. L., Roach, S., and Wickstrom, G. 2003. Transformation-oriented programming: A development methodology for high assurance software. In Advances in Computers: Highly Dependable Software, M. Zelkowitz, Ed. vol. 58. 47--116.]]","journal-title":"Ed."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1196636.1196639","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T19:21:42Z","timestamp":1672255302000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1196636.1196639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":25,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["10.1145\/1196636.1196639"],"URL":"https:\/\/doi.org\/10.1145\/1196636.1196639","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,11]]},"assertion":[{"value":"2006-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}