{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:49:09Z","timestamp":1760597349968},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881933"},{"type":"electronic","value":"9783540881940"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-88194-0_15","type":"book-chapter","created":{"date-parts":[[2008,10,17]],"date-time":"2008-10-17T10:56:21Z","timestamp":1224240981000},"page":"226-237","source":"Crossref","is-referenced-by-count":14,"title":["Partial Translation Verification for Untrusted Code-Generators"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Staats","sequence":"first","affiliation":[]},{"given":"Mats P. E.","family":"Heimdahl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A. Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electronic Notes in Theoretical Computer Science\u00a066(2), 160\u2013177 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"15_CR2","first-page":"118","volume":"58","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers\u00a058, 118\u2013149 (2003)","journal-title":"Advances in Computers"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988. Springer, Heidelberg (2004)"},{"issue":"5","key":"15_CR4","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/358438.349315","volume":"35","author":"C. Colby","year":"2000","unstructured":"Colby, C., Lee, P., Necula, G.C., Blau, F., Plesko, M., Cline, K.: A certifying compiler for Java. ACM SIGPLAN Notices\u00a035(5), 95\u2013107 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Denney, E., Fischer, B.: Annotation inference for the safety certification of automatically generated code. In: Proceedings of the 21st IEEE International Conference on Automated Software Engineering (ASE 2006), pp. 265\u2013268 (2006)","DOI":"10.1109\/ASE.2006.15"},{"key":"15_CR6","unstructured":"Duret-Lutz, A., Poitrenaud, D.: SPOT: an extensible model checking library using transition-based generalized Bu\/spl uml\/chi automata. In: Proceedings of the IEEE Computer Society\u2019s 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004 (MASCOTS 2004), pp. 76\u201383 (2004)"},{"key":"15_CR7","unstructured":"Dybjer, P.: Using Domain Algebras to Prove the Correctness of a Compiler. Springer, Heidelberg"},{"key":"15_CR8","unstructured":"Esterel-Technologies. SCADE Suite product description (2004), http:\/\/www.esterel-technologies.com\/v2\/scadeSuiteForSafetyCriticalSoftwareDevelopment\/index.html"},{"issue":"19-32","key":"15_CR9","first-page":"1","volume":"19","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer Science\u00a019(19-32), 1 (1967)","journal-title":"Mathematical Aspects of Computer Science"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV","author":"R. Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pp. 3\u201318. Chapman & Hall, Ltd., Boca Raton (1996)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-Based Verification of Temporal Properties on Running Programs. In: Proceedings of International Conference on Automated Software Engineering (ASE 2001), pp. 412\u2013416 (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to Buchi automata. In: Proceedings of the 22nd IFIP WG, pp. 6 (2002)","DOI":"10.1007\/3-540-36135-9_20"},{"issue":"1","key":"15_CR13","first-page":"5","volume":"8","author":"J.D. Guttman","year":"1995","unstructured":"Guttman, J.D., Ramsdell, J.D., Wand, M.: VLISP: A verified implementation of Scheme. Higher-Order and Symbolic Computation\u00a08(1), 5\u201332 (1995)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"15_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45213-3_4","volume-title":"Modular Programming Languages","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research. In: B\u00f6sz\u00f6rm\u00e9nyi, L., Schojer, P. (eds.) JMLC 2003. LNCS, vol.\u00a02789. Springer, Heidelberg (2003)"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/11563228_10","volume-title":"Computer Safety, Reliability, and Security","author":"A. Joshi","year":"2005","unstructured":"Joshi, A., Heimdahl, M.P.E.: Model-Based Safety Analysis of Simulink Models Using SCADE Design Verifier. In: Winther, R., Gran, B.A., Dahll, G. (eds.) SAFECOMP 2005. LNCS, vol.\u00a03688, pp. 122\u2013135. Springer, Heidelberg (2005)"},{"key":"15_CR16","unstructured":"Mathworks Inc. Simulink product web site, http:\/\/www.mathworks.com\/products\/simulink"},{"key":"15_CR17","unstructured":"Mathworks Inc. Stateflow product web site, http:\/\/www.mathworks.com"},{"key":"15_CR18","first-page":"21","volume":"62","author":"J. McCarthy","year":"1962","unstructured":"McCarthy, J.: Towards a mathematical science of computation. Information Processing\u00a062, 21\u201328 (1962)","journal-title":"Information Processing"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Miller, S.P., Anderson, E.A., Wagner, L.G., Whalen, M.W., Heimdahl, M.P.E.: Formal Verification of Flight Critical Software. In: Proceedings of the AIAA Guidance, Navigation and Control Conference and Exhibit (August 2005)","DOI":"10.2514\/6.2005-6431"},{"issue":"4","key":"15_CR20","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10009-004-0173-6","volume":"8","author":"S.P. Miller","year":"2006","unstructured":"Miller, S.P., Tribble, A.C., Whalen, M.W., Heimdahl, M.P.E.: Proving the shalls: Early validation of requirements through formal methods. Int. J. Softw. Tools Technol. Transf.\u00a08(4), 303\u2013319 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"15_CR21","first-page":"461","volume":"5","author":"J.S. Moore","year":"1989","unstructured":"Moore, J.S.: A mechanically verified language implementation. Journal of Automated Reasoning\u00a05(4), 461\u2013492 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"5","key":"15_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/277652.277752","volume":"33","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. ACM SIGPLAN Notices\u00a033(5), 333\u2013344 (1998)","journal-title":"ACM SIGPLAN Notices"},{"key":"15_CR23","unstructured":"The NuSMV Toolset (2005), http:\/\/nusmv.irst.itc.it\/"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS, vol.\u00a098, pp. 151\u2013166","DOI":"10.1007\/BFb0054170"},{"key":"15_CR25","unstructured":"Rinard, M.: Credible compilation. In: Proceedings of the FLoC Workshop Run-Time Result Verification (July 1999)"},{"key":"15_CR26","unstructured":"ARP 4761: Guidelines and Methods for Conducting the Safety Assessment Process on Civil Airborne Systems and Equipment. SAE International (December 1996)"},{"key":"15_CR27","unstructured":"Wheeler, D.: SLOCCount: Source Lines of Code Count. Webpage. Version, 2 (2004)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88194-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T15:08:19Z","timestamp":1557846499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88194-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881933","9783540881940"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88194-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}