{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:25:08Z","timestamp":1754483108328},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664628"},{"type":"electronic","value":"9783540482574"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_8","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T16:25:09Z","timestamp":1184948709000},"page":"137-150","source":"Crossref","is-referenced-by-count":3,"title":["Translation Validation: From DC+ 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","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2), 1991.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"A. Benviniste, P. Le Guernic, and C. Jacquemot. Synchronous programming with events and relations: the SIGNAL language. Science of Computer Programming, 16, 1991.","DOI":"10.1016\/0167-6423(91)90001-E"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"G. Berry and G. Gonthier. The ESTEREL synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2), 1992.","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger, E. Gr\u00e4del, and Y. Gurevich. The Classical Decision Problem. Springer, 1996.","DOI":"10.1007\/978-3-642-59207-2"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"P. Caspi, N. Halbwachs, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE, 79(9), 1991.","DOI":"10.1109\/5.97300"},{"key":"8_CR6","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"A. Cimatti","year":"1997","unstructured":"A. Cimatti, F. Giunchiglia, and P. Pecchiari et al. A provably correct embedded verifier for the certification of safety critical software. In CAV, number 1254 in LNCS. Springer, 1997."},{"key":"8_CR7","unstructured":"The declarative code DC+. ESPRIT Project: SACRES, Project Report, 1997. Version 1.3."},{"key":"8_CR8","unstructured":"Another look at real-time programming, volume 9 of Proc. of the IEEE, September 1991."},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084815","volume-title":"Proceedings CONCUR","author":"F. Maraninchi","year":"1992","unstructured":"F. Maraninchi. Operational and compositional semantics of synchronous automata compositions. In Proceedings CONCUR, volume 630 of LNCS. Springer, 1992."},{"key":"8_CR10","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u2019 98","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli, M. Siegel, and O. Shtrichman. Translation validation for synchronous languages. In ICALP\u2019 98, LNCS. Springer-Verlag, 1998."},{"key":"8_CR11","series-title":"Lect Notes Comput Sci","volume-title":"TACAS 98: Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli, M. Siegel, and E. Singermann. Translation validation. In TACAS 98: Tools and Algorithms for the Construction and Analysis of Systems, LNCS. Springer-Verlag, 1998."},{"key":"8_CR12","unstructured":"private communications with TNI (BREST), Siemens (Munich) and Inria (Rennes)."}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T07:08:00Z","timestamp":1556694480000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}