{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:46:47Z","timestamp":1725893207214},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540773948"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-77395-5_12","type":"book-chapter","created":{"date-parts":[[2007,12,6]],"date-time":"2007-12-06T11:25:53Z","timestamp":1196940353000},"page":"139-150","source":"Crossref","is-referenced-by-count":4,"title":["Translation Validation of System Abstractions"],"prefix":"10.1007","author":[{"given":"Jan Olaf","family":"Blech","sequence":"first","affiliation":[]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Adler, R., Schaefer, I., Schuele, T., Vecchie, E.: From Model-Based Design to Formal Verification of Adaptive Embedded Systems. In: Proc. of ICFEM 2007, (November 2007)","DOI":"10.1007\/978-3-540-76650-6_6"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/3-540-56496-9_21","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1993","unstructured":"Bensalem, S., Bouajjani, A., Loiseaux, C., Sifakis, J.: Property preserving simulations. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 260\u2013273. Springer, Heidelberg (1993)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Blech, J.O., Gesellensetter, L., Glesner, S.: Formal Verification of Dead Code Elimination in Isabelle\/HOL. In: Proc. of SEFM, pp. 200\u2013209 (2005)","DOI":"10.1109\/SEFM.2005.20"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Blech, J.O., Poetzsch-Heffter, A.: A certifying code generation phase. In: Proc. of COCV 2007 ENTCS, Braga, Portugal, (March 2007)","DOI":"10.1016\/j.entcs.2007.09.008"},{"key":"12_CR5","unstructured":"Blech, J.O., Schaefer, I., Poetzsch-Heffter, A.: On Translation Validation for System Abstractions. Technical Report 361-07, TU Kaiserslautern, (July 2007)"},{"issue":"5","key":"12_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM TOPLAS\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM TOPLAS"},{"key":"12_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"12_CR8","first-page":"238","volume-title":"Proc. of POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL, pp. 238\u2013252. ACM Press, New York ( January 1977)"},{"key":"12_CR9","first-page":"269","volume-title":"Proc. of POPL","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. of POPL, pp. 269\u2013282. ACM Press, New York (January 1979)"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst.\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR11","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Elsevier, Amsterdam (1990)"},{"key":"12_CR12","unstructured":"Gawkowski, M.J., Blech, J.O., Poetzsch-Heffter, A.: Certifying Compilers based on Formal Translation Contracts. Technical Report 355-06, TU Kaiserslautern (November 2006)"},{"key":"12_CR13","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proc. of IJCAI, pp. 481\u2013489 (1971)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, Springer, Heidelberg (1998)"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2005.03.023","volume":"132","author":"A. Poetzsch-Heffter","year":"2005","unstructured":"Poetzsch-Heffter, A., Gawkowski, M.J.: Towards proof generating compilers. Electronics Notes in Theoritical Computer Science\u00a0132(1), 37\u201351 (2005)","journal-title":"Electronics Notes in Theoritical Computer Science"},{"key":"12_CR17","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proc. of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, (July 1999)"},{"key":"12_CR18","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Theorem Proving in Higher Order Logics, Springer, Heidelberg (2004)"},{"issue":"3","key":"12_CR19","first-page":"223","volume":"9","author":"L. Zuck","year":"2003","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science\u00a09(3), 223\u2013247 (2003)","journal-title":"Journal of Universal Computer Science"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77395-5_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:10:31Z","timestamp":1619521831000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77395-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540773948"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77395-5_12","relation":{},"subject":[]}}