{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:15:58Z","timestamp":1778249758739,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540666240","type":"print"},{"value":"9783540480921","type":"electronic"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48092-7_11","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T13:01:46Z","timestamp":1186750906000},"page":"231-255","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Translation Validation: From SIGNAL to C"],"prefix":"10.1007","author":[{"given":"A.","family":"Pnueli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Shtrichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Siegel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,3,24]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, May 1991.","journal-title":"Theoretical Computer Science"},{"key":"11_CR2","unstructured":"W. Ackerman. Solvable cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954."},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"A. Benveniste, P. Le Guernic, and C. J acquemot.Synchronous programming with events and relations: the SIGNAL languages and its semantics. Science of Computer Programming, 16:103\u2013149, 1991.","journal-title":"Science of Computer Programming"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger, E. Gr\u00e4del, and Y. Gurevich. The Classical Decision Problem. Springer-Verlag,1996.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"B. Buth, K.-H. Buth, M. Fr\u00e4nzle, B. von Karger, Y. Lakhneche, H. Langmaack, and M. M\u00fcller-Olm.Provably correct compiler development and implementation. In U. Kastens and P. Pfahler, editors, Compiler Construction\u201892, 4th International Conference Paderborn, Germany, volume 641 of Lect. Notes in Comp. Sci., pages 141\u2013155. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55984-1_14"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design: a Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano, P. Traverso, and B. Yu. A provably correct embedded verifier for the certification of safety critical software. In O. Grumberg, editor, Proc. 9th Intl. Conference on Computer Aided Verification (CAV\u201897), volume 1254 of Lect. Notes in Comp. Sci., pages 202\u2013213. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63166-6_21"},{"key":"11_CR8","unstructured":"A. Cimatti, F. Giunchiglia, P. Traverso, and A. Villafiorita.Run-time result formal verification of safety critical software: an industrial case study. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"D.L. Clutterbuck and B.A. Carre. The verification of low-level code. Software Engineering Journal, pages 97\u2013111, 1998.","DOI":"10.1049\/sej.1988.0012"},{"key":"11_CR10","unstructured":"P. Curzon. A verified compiler for a structured assembly language. In international workshop on the HOL theorem Proving System and its applications. IEEE Computer Society Press, 1991."},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BF01128407","volume":"8","author":"J.D. Guttman","year":"1995","unstructured":"J.D. Guttman, J.D. Ramsdell, and V. Swarup. The VLISP verified Scheme system. Lisp and Symbolic Computation, 8:33\u2013100, 1995.","journal-title":"Lisp and Symbolic Computation"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01128406","volume":"8","author":"J.D. Guttman","year":"1995","unstructured":"J.D. Guttman, J.D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5\u201332, 1995.","journal-title":"Lisp and Symbolic Computation"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"M. M\u00fcller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, volume 1283 of Lect. Notes in Comp. Sci. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0027453"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BF01128408","volume":"8","author":"D.P. Oliva","year":"1995","unstructured":"D.P. Oliva, J.D. Ramsdell, and M. Wand. The VLISP verified PreScheme compiler. Lisp and Symbolic Computation, 8:111\u2013182, 1995.","journal-title":"Lisp and Symbolic Computation"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"I.M. O\u2018Neill, D.L. Clutterbuck, and P.F. Farrow. The formal verification of safetycritical a ssembly code. In IFAC Symposium on safety of computer control systems, 1988.","DOI":"10.1016\/S1474-6670(17)54540-1"},{"key":"11_CR16","unstructured":"Private communications with TNI (BREST), Siemens (Munich) and Inria (Rennes)."},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small-domains instantiations. In N. Halbwachs and D. Peled, editors, Proc. 11st Intl. Conference on Computer Aided Verification (CAV\u201899), Lect. Notes in Comp. Sci. Springer-Verlag, 1999. to appear.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. In R. Alur and T. Henzinger, editors, Proc. 8\n                           \n                    th\n                  \n                           Intl. Conference on Computer Aided Verirication (CAV\u201896), Lect. Notes in Comp. Sci., pages 184\u2013195. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_68"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and O. Shtrichman. The code validation tool (CVT)-automatic verification of a compilation process. Software Tools for Technology Transfer, 2, 1999.","DOI":"10.1007\/s100090050027"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In B. Steffen, editor, 4th Intl. Conf. TACAS\u201898, volume 1384 of Lect. Notes in Comp. Sci., pages 151\u2013166. Springer-Verlag, 1998.","DOI":"10.1007\/BFb0054170"},{"key":"11_CR21","unstructured":"A. Stump and D. Dill. Generating proofs from a decision procedure. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999."},{"key":"11_CR22","unstructured":"P. Traverso and P. Bertoli. Mechanized result verification: an industrial application. In Run-Time Result Verification. The 1999 Federated Logic Conference, 1999."}],"container-title":["Lecture Notes in Computer Science","Correct System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48092-7_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:49:19Z","timestamp":1778248159000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-48092-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540666240","9783540480921"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48092-7_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"24 March 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}