{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:51:55Z","timestamp":1761929515957},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642161445"},{"type":"electronic","value":"9783642161452"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16145-2_12","type":"book-chapter","created":{"date-parts":[[2010,9,21]],"date-time":"2010-09-21T07:41:31Z","timestamp":1285054891000},"page":"166-180","source":"Crossref","is-referenced-by-count":6,"title":["Verifying Semantic Conformance of State Machine-to-Java Code Generators"],"prefix":"10.1007","author":[{"given":"Lukman","family":"Ab Rahim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jon","family":"Whittle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"12_CR1","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W. Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J., Lerda, F.: Model checking programs. Automated Software Engineering Journal\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering Journal"},{"key":"12_CR2","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"Proceedings of the 24th ACM SIGPLAN-SIGACT 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 symposium on Principles of programming languages (POPL 1997), pp. 106\u2013119. ACM, New York (1997)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/10722167_44","volume-title":"Computer Aided Verification","author":"C. Colby","year":"2000","unstructured":"Colby, C., Lee, P., Necula, G.C.: A Proof-Carrying Code Architecture for Java. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 557\u2013560. Springer, Heidelberg (2000)"},{"key":"12_CR4","first-page":"1","volume-title":"Proceedings of the 36th Annual Hawaii International Conference on System Sciences","author":"J. Schumann","year":"2003","unstructured":"Schumann, J., Fischer, B., Whalen, M., Whittle, J.: Certification Support for Automatically Generated Programs. In: Proceedings of the 36th Annual Hawaii International Conference on System Sciences, pp. 1\u201310. IEEE, Los Alamitos (2003)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1109\/ISoLA.2006.76","volume-title":"2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006)","author":"E. Denney","year":"2006","unstructured":"Denney, E., Fischer, B.: Extending Source Code Generators for Evidence-Based Software Certification. In: 2nd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2006), pp. 138\u2013145. ACM, New York (2006)"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/1449913.1449926","volume-title":"Proceedings of the 7th International Conference on Generative Programming and Component Engineering (GPCE 2008)","author":"E. Denney","year":"2008","unstructured":"Denney, E., Fischer, B.: Generating Customized Verifiers for Automatically Generated Code. In: Proceedings of the 7th International Conference on Generative Programming and Component Engineering (GPCE 2008), pp. 77\u201388. ACM, New York (2008)"},{"key":"12_CR7","unstructured":"IBM: Rational Rhapsody, \n                    \n                      http:\/\/www-01.ibm.com\/software\/rational\/products\/rhapsody\/developer\/"},{"key":"12_CR8","unstructured":"Visual Paradigm International: Visual paradigm, \n                    \n                      http:\/\/www.visual-paradigm.com\/"},{"key":"12_CR9","unstructured":"OMG: Unified Modeling Language: Superstructure version 2.1.1. OMG (February 2007)"},{"key":"12_CR10","unstructured":"Varr\u00f3, D., Pataricza, A.: Automated formal verification of model transformations. In: J\u00fcrjens, J., Rumpe, B., France, R., Fernandez, E.B. (eds.) CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML 2003 Workshop. Number TUM-I0323 in Technical Report, Technische Universit\u00e4t M\u00fcnchen, pp. 63\u201378 (September 2003)"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-540-88194-0_15","volume-title":"Formal Methods and Software Engineering","author":"M. Staats","year":"2008","unstructured":"Staats, M., Heimdahl, M.: Partial Translation Verification for Untrusted Code-Generators. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 226\u2013237. Springer, Heidelberg (2008)"},{"key":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1007\/978-3-540-75209-7_45","volume-title":"Model Driven Engineering Languages and Systems","author":"S. Chaki","year":"2007","unstructured":"Chaki, S., Ivers, J., Lee, P., Wallnau, K., Zeillberger, N.: Model-Driven Construction of Certified Binaries. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol.\u00a04735, pp. 666\u2013681. Springer, Heidelberg (2007)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: The Code Validation Tool CVT: Automatic Verification of a Compilation Process. Software Tools for Technology Transfer\u00a02, 192\u2013201 (1998)","journal-title":"Software Tools for Technology Transfer"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Barbosa, P.E.S., Ramalho, F., de Figueiredo, J.C.A., dos Jr., A.D.S.: An extended MDA architecture for ensuring semantics-preserving transformations. In: 32nd Annual IEEE Software Engineering Workshop, pp. 33\u201342 (October 2008)","DOI":"10.1109\/SEW.2008.8"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/AERO.2005.1559605","volume-title":"IEEE Aerospace Conference","author":"E. Denney","year":"2005","unstructured":"Denney, E., Fischer, B., Schumann, J., Richardson, J.: Automatic Certification of Kalman Filters for Reliable Code Generation. In: IEEE Aerospace Conference, pp. 1\u201310. IEEE, Los Alamitos (2005)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-70881-0_9","volume-title":"Perspectives of Systems Informatics","author":"T. Baar","year":"2007","unstructured":"Baar, T., Markovi\u0107, S.: A graphical approach to prove the semantic preservation of UML\/OCL refactoring rules. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol.\u00a04378, pp. 70\u201383. Springer, Heidelberg (2007)"},{"key":"12_CR17","unstructured":"Whittle, J., Gajanovic, B.: Model transformations should be more than just model generators. In: Briand, L.C., Williams, C. (eds.) MoDELS 2005. LNCS, vol.\u00a03713, pp. 32\u201338. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"12_CR18","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s11334-009-0108-1","volume":"6","author":"M. Egea","year":"2010","unstructured":"Egea, M., Rusu, V.: Formal executable semantics for conformance in the MDE framework. Innovations System Software Engineering\u00a06(1-2), 73\u201381 (2010)","journal-title":"Innovations System Software Engineering"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16145-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:01:36Z","timestamp":1558292496000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16145-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642161445","9783642161452"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16145-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}