{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:15Z","timestamp":1725540495827},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_27","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"521-540","source":"Crossref","is-referenced-by-count":6,"title":["Machine-Checked Sequencer for Critical Embedded Code Generator"],"prefix":"10.1007","author":[{"given":"Nassima","family":"Izerrouken","sequence":"first","affiliation":[]},{"given":"Marc","family":"Pantel","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Thirioux","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-77442-6_2","volume-title":"Practical Aspects of Declarative Languages","author":"B. Pagano","year":"2008","unstructured":"Pagano, B., Andrieu, O., Canou, B., Chailloux, E., Colaco, J.L., Moniot, T., Wang, P.: Certified development tools implementation in objective caml. In: Hudak, P., Warren, D.S. (eds.) PADL 2008. LNCS, vol.\u00a04902, pp. 2\u201317. Springer, Heidelberg (2008)"},{"issue":"1","key":"27_CR2","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0167-6423(99)00015-5","volume":"36","author":"G. Berry","year":"2000","unstructured":"Berry, G., Bouali, A., Fornari, X., Ledinot, E., Nassor, E., de Simone, R.: Esterel: a formal method applied to avionic software development. Sci. Comput. Program.\u00a036(1), 5\u201325 (2000)","journal-title":"Sci. Comput. Program."},{"key":"27_CR3","unstructured":"Izerrouken, N., Thirioux, X., Pantel, M., Strecker, M.: Certifying an Automated Code Generator Using Formal Tools: Preliminary Experiments in the GeneAuto Project. In: European Congress on Embedded Real-Time Software (ERTS), Toulouse, 29\/01\/2008-01\/02\/2008 (2008) (electronic medium), http:\/\/www.sia.fr"},{"key":"27_CR4","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Colaco, J.L., Hamon, G., Pouzet, M.: Clock-directed modular code generation of synchronous data-flow languages. In: ACM International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES), Tuscon, Arizona (June 2008)","DOI":"10.1145\/1375657.1375674"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Caspi, P., Hamon, G., Pouzet, M.: Synchronous Functional Programming with Lucid Synchrone. In: Real-Time Systems: Models and verification \u2014Theory and tools. ISTE (2007)","DOI":"10.1002\/9780470611012.ch7"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.L., Hamon, G., Pouzet, M.: Mixing signals and modes in synchronous data-flow systems. In: ACM International Conference on Embedded Software (EMSOFT 2006), Seoul, South Korea (October 2006)","DOI":"10.1145\/1176887.1176899"},{"issue":"3","key":"27_CR8","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10009-004-0160-y","volume":"6","author":"J.L. Cola\u00e7o","year":"2004","unstructured":"Cola\u00e7o, J.L., Pouzet, M.: Type-based initialization analysis of a synchronous data-flow language. International Journal on Software Tools for Technology Transfer (STTT)\u00a06(3), 245\u2013255 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/978-3-540-45212-6_7","volume-title":"Embedded Software","author":"P. Caspi","year":"2003","unstructured":"Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S.: Translating discrete-time simulink to lustre. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 84\u201399. Springer, Heidelberg (2003)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Caspi, P., Curic, A., Maignan, A., Sofronis, C., Tripakis, S., Niebert, P.: From simulink to scade\/lustre to tta: a layered approach for distributed embedded applications. In: ACM-SIGPLAN Languages, Compilers, and Tools for Embedded Systems, LCTES 2003 (2003)","DOI":"10.1145\/780732.780754"},{"issue":"1","key":"27_CR11","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.9999","volume":"163","author":"A. Benveniste","year":"2000","unstructured":"Benveniste, A., Caillaud, B., Guernic, P.L.: Compositionality in dataflow synchronous languages: specification and distributed code generation 1, 2, 3. Information and Computation\u00a0163(1), 125\u2013171 (2000)","journal-title":"Information and Computation"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Raymond, P., Ratel, C.: Generating efficient code from data-flow programs. In: Third International Symposium on Programming Language Implementation and Logic Programming, Passau, Germany (August 1991)","DOI":"10.1007\/3-540-54444-5_100"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","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.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"issue":"5","key":"27_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validator for optimizing compilers. SIGPLAN Not.\u00a035(5), 83\u201394 (2000)","journal-title":"SIGPLAN Not."},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal Certification of a Compiler Back-end or Programming a compiler with a Proof Assistant. In: POPL 2006, 33rd Symposium on Principles of Programming Languages (January 2006)","DOI":"10.1145\/1111037.1111042"}],"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-642-10373-5_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,17]],"date-time":"2024-03-17T17:12:13Z","timestamp":1710695533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}