{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T04:34:09Z","timestamp":1747888449520,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466742"},{"type":"electronic","value":"9783662466759"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46675-9_12","type":"book-chapter","created":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T20:24:38Z","timestamp":1427833478000},"page":"171-185","source":"Crossref","is-referenced-by-count":1,"title":["Translation Validation for Clock Transformations in a Synchronous Compiler"],"prefix":"10.1007","author":[{"given":"Van Chan","family":"Ngo","sequence":"first","affiliation":[]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[]},{"given":"Thierry","family":"Gautier","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Le Guernic","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Study in Logic and the Foundations of Mathematics","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackerman","year":"1954","unstructured":"Ackerman, W.: Solvable Cases of the Decision Problem. Study in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Berry, G.: The Foundations of Esterel. In: Proof, Language and Interaction: Essay in Honor of Robin Milner, MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Borger, E., Gradel, E., Gurevich, Y.: The Classical Decision Problem. Spinger-Verlag (1996)","DOI":"10.1007\/978-3-642-59207-2"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Besnard, L., Gautier, T., Le Guernic, P., Talpin, J.-P.: Compilation of Polychronous Data Flow Equations. In: Synthesis of Embedded Software. Springer (2010)","DOI":"10.1007\/978-1-4419-6400-7_1"},{"issue":"5","key":"12_CR5","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1109\/9.53519","volume":"35","author":"A. Benveniste","year":"1990","unstructured":"Benveniste, A., LeGuernic, P.: Hybrid Dynamical Systems Theory and the Signal Language. IEEE Transactions on Automatic Control\u00a035(5), 535\u2013546 (1990)","journal-title":"IEEE Transactions on Automatic Control"},{"issue":"8","key":"12_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers, C"},{"key":"12_CR7","unstructured":"Inria, The CompCert Project, http:\/\/compcert.inria.fr"},{"key":"12_CR8","unstructured":"Inria, The Coq Proof Assitant, http:\/\/coq.inria.fr"},{"key":"12_CR9","unstructured":"Dutertre, B., de Moura, L.: Yices Sat-solver (2009), http:\/\/yices.csl.ri.com"},{"key":"12_CR10","unstructured":"Gamati\u00e9, A.: Designing Embedded Systems with the Signal Programming Language: Synchronous, Reactive Specification, pp. 971\u2013978. Springer, New York (2009) ISBN 978-1-4419-0940-4"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Functional Programming Languages and Computer Architecture","year":"1987","unstructured":"Kahn, G. (ed.): FPCA 1987. LNCS, vol.\u00a0274. Springer, Heidelberg (1987)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Gamati\u00e9, A., Gonnord, L.: Static Analysis of Synchronous Programs in Signal for Efficient Design of Multi-Clocked Embedded Systems. In: ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, Tools and Theory for Embedded Systems - LCTES 2011, Chicago, IL, USA (April 2011)","DOI":"10.1145\/1967677.1967688"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Halbwachs, N.: A Synchronous Language at Work: the Story of Lustre. In: 3th ACM-IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2005 (July 2005)","DOI":"10.1109\/MEMCOD.2005.1487884"},{"key":"12_CR14","unstructured":"Le Guernic, P., Gautier, T.: Advanced Topics in Data-flow Computing, Chapter Data-flow to von Neumann: the Signal Approach, pp. 413\u2013438. Prentice-Hall (1991)"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal Certification of a Compiler Back-end, or Programming a Compiler with a Proof Assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation Validation for an Optimizing Compiler. In: Proceeding PLDI 2000 Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 83\u201394 (May 2000)","DOI":"10.1145\/358438.349314"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-30729-4_9","volume-title":"Integrated Formal Methods","author":"V.C. Ngo","year":"2012","unstructured":"Ngo, V.C., Talpin, J.-P., Gautier, T., Le Guernic, P., Besnard, L.: Formal Verification of Compiler Transformations on Polychronous Equations. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol.\u00a07321, pp. 113\u2013127. Springer, Heidelberg (2012)"},{"key":"12_CR18","unstructured":"Ngo, V.C.: Formal Verification of a Synchronous Data-flow Compiler: from Signal to C. In: PhD thesis (2014)"},{"key":"12_CR19","unstructured":"Inria\/Espresso, Polychrony Toolset, http:\/\/www.irisa.fr\/espresso\/Polychrony"},{"key":"12_CR20","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)"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-48092-7_11","volume-title":"Correct System Design","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: Translation Validation: From Signal to C. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 231\u2013255. Springer, Heidelberg (1999)"},{"key":"12_CR22","unstructured":"RTCA, DO-178C, http:\/\/rtca.org"},{"key":"12_CR23","unstructured":"Stump, A., Deters, M.: SMT-Comp (2009), http:\/\/www.smtcomp.org\/2009"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating Value-graph Translation Validation for LLVM. In: ACM SIGPLAN Conference on Programming and Language Design Implementation, California (June 2011)","DOI":"10.1145\/1993498.1993533"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Leroy, X.: A Simple, Verified Validator for Software Pipelining. In: 37th Principles of Programming Languages, pp. 83\u201392. ACM Press (2010)","DOI":"10.1145\/1706299.1706311"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46675-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T19:47:46Z","timestamp":1747856866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46675-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466742","9783662466759"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46675-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}