{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T22:08:05Z","timestamp":1791065285133,"version":"4.1.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2013,9,13]],"date-time":"2013-09-13T00:00:00Z","timestamp":1379030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s11704-013-3910-8","type":"journal-article","created":{"date-parts":[[2013,9,13]],"date-time":"2013-09-13T06:21:42Z","timestamp":1379053302000},"page":"598-616","source":"Crossref","is-referenced-by-count":7,"title":["Formal verification of synchronous data-flow program transformations toward certified compilers"],"prefix":"10.1007","volume":"7","author":[{"given":"Van Chan","family":"Ngo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thierry","family":"Gautier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Le Guernic","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lo\u00efc","family":"Besnard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,9,13]]},"reference":[{"key":"3910_CR1","first-page":"425","volume-title":"Proof, Language, and Interaction","author":"G Berry","year":"2000","unstructured":"Berry G. The foundations of Esterel. In: Proof, Language, and Interaction. 2000, 425\u2013454"},{"key":"3910_CR2","first-page":"3","volume-title":"Proceedings of the 3rd ACM and IEEE International Conference on Formal Methods and Models for Co-Design","author":"N Halbwachs","year":"2005","unstructured":"Halbwachs N. A synchronous language at work: the story of lustre. In: Proceedings of the 3rd ACM and IEEE International Conference on Formal Methods and Models for Co-Design. 2005, 3\u201311"},{"key":"3910_CR3","volume-title":"Designing embedded systems with the Signal programming language: synchronous, reactive specification","author":"A Gamati","year":"2009","unstructured":"Gamati A. Designing embedded systems with the Signal programming language: synchronous, reactive specification. Springer Publishing Company, Incorporated, 2009"},{"key":"3910_CR4","unstructured":"Inria. The coq proof assitant. http:\/\/coq.inria.fr"},{"key":"3910_CR5","unstructured":"Do-178c. http:\/\/rtca.org"},{"key":"3910_CR6","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. Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1998-151-166"},{"key":"3910_CR7","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/3-540-48092-7_11","volume":"1710","author":"A Pnueli","year":"1999","unstructured":"Pnueli A, Shtrichman O, Siegel M. Translation validation: from Signal to C. Lecture Notes in Computer Science, 1999,1710: 231\u2013255","journal-title":"Lecture Notes in Computer Science"},{"key":"3910_CR8","unstructured":"Inria. The compcert project. http:\/\/compcert.inria.fr"},{"issue":"5","key":"3910_CR9","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G C Necula","year":"2000","unstructured":"Necula G C. Translation validation for an optimizing compiler. ACM SIGPLAN Notices, 2000, 35(5): 83\u201394","journal-title":"ACM SIGPLAN Notices"},{"key":"3910_CR10","first-page":"295","volume-title":"ACM Sigplan Notices","author":"J B Tristan","year":"2011","unstructured":"Tristan J B, Govereau P, Morrisett G. Evaluating value-graph translation validation for LLVM. ACM Sigplan Notices, 2011, 295\u2013305"},{"key":"3910_CR11","unstructured":"Dutertre B, Moura de L. Yices Sat-solver. http:\/\/yices.csl.ri.com"},{"key":"3910_CR12","unstructured":"Espresso, Polychrony toolset. http:\/\/www.irisa.fr\/espresso\/Polychrony"},{"issue":"5","key":"3910_CR13","doi-asserted-by":"crossref","first-page":"535","DOI":"10.1109\/9.53519","volume":"35","author":"A Benveniste","year":"1990","unstructured":"Benveniste A, Le Guernic P. Hybrid dynamical systems theory and the signal language. IEEE Transactions on Automatic Control, 1990, 35(5): 535\u2013546","journal-title":"IEEE Transactions on Automatic Control"},{"key":"3910_CR14","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/3-540-18317-5_15","volume":"274","author":"T Gautier","year":"1987","unstructured":"Gautier T, Le Guernic P, Besnard L. Signal: a declarative language for synchronous programming of real-time systems. Lecture Notes in Computer Science, 1987, 274: 257\u2013277","journal-title":"Lecture Notes in Computer Science"},{"key":"3910_CR15","first-page":"1","volume-title":"Handbook of Logic in Computer Science: Volume 3: Semantic Structures","author":"S Abramsky","year":"1994","unstructured":"Abramsky S, Jung A. Domain theory. Abramsky S, Gabbay D M, Maibaum T S E, ed(s). Handbook of Logic in Computer Science: Volume 3: Semantic Structures. Oxford: Clarendon Press, 1994, 1\u2013168"},{"key":"3910_CR16","first-page":"471","volume-title":"IFIP Congress","author":"G Kahn","year":"1974","unstructured":"Kahn G. The semantics of a simple language for parallel programming. IFIP Congress, 1974, 471\u2013475"},{"key":"3910_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-1-4419-6400-7_1","volume-title":"Synthesis of Embedded Software","author":"L Besnard","year":"2010","unstructured":"Besnard L, Gautier T, Le Guernic P, Talpin J P. Compilation of polychromous data flow equations. Synthesis of Embedded Software, Springer, 2010, 1\u201340"},{"key":"3910_CR18","unstructured":"Ackermann W. Solvable Cases of the Decision Problem. Vol. 12. North-Holland Pub. Co., 1954"},{"key":"3910_CR19","unstructured":"Le Guernic P, Gautier T. Data-flow to von neumann: the signal approach. Rapports de recherche-INRIA"},{"issue":"5","key":"3910_CR20","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1145\/2016603.1967688","volume":"46","author":"A Gamati\u00e9","year":"2011","unstructured":"Gamati\u00e9 A, Gonnord L. Static analysis of synchronous programs in signal for effcient design of multi-clocked embedded systems. ACM Sigplan Notices, 2011, 46(5): 71\u201380","journal-title":"ACM Sigplan Notices"},{"key":"3910_CR21","first-page":"1","volume-title":"ACM SIGPLAN Notices","author":"F E Allen","year":"1970","unstructured":"Allen F E. Control flow analysis. ACM SIGPLAN Notices, 1970, 1\u201319"},{"key":"3910_CR22","unstructured":"Biere A, Heule M, Maaren v H, Walsh T. Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, 2009"},{"key":"3910_CR23","first-page":"99","volume-title":"Lecture Notes in Computer Science","author":"O Ma-e\u00efs","year":"1993","unstructured":"Ma-e\u00efs O, Le Guernic P. Combining dependability with architectural adaptability by means of the signal language. Lecture Notes in Computer Science, 1993(724): 99\u2013110"},{"key":"3910_CR24","volume-title":"The satisfiability modulo theories library (SMT-LIB)","author":"C Barrett","year":"2008","unstructured":"Barrett C, Ranise S, Stump A, Tinelli C. The satisfiability modulo theories library (SMT-LIB). http:\/\/www.SMT-LIB.org , 2008"},{"key":"3910_CR25","unstructured":"http:\/\/www.smtcomp.org\/2009"},{"issue":"8","key":"3910_CR26","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"R E Bryant","year":"1986","unstructured":"Bryant R E. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 1986, 100(8): 677\u2013691","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"3910_CR27","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1145\/1111320.1111042","volume":"41","author":"X Leroy","year":"2006","unstructured":"Leroy X. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. ACM SIGPLAN Notices, 2006, 41(1): 42\u201354","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"3910_CR28","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/1707801.1706311","volume":"45","author":"J B Tristan","year":"2010","unstructured":"Tristan J B, Leroy X. A simple, verified validator for software pipelining. ACM SIGPLAN Notices, 2010, 45(1):83\u201392","journal-title":"ACM SIGPLAN Notices"},{"issue":"7","key":"3910_CR29","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/1379023.1375674","volume":"43","author":"D Biernacki","year":"2008","unstructured":"Biernacki D, Cola\u00e7o J L, Hamon G, Pouzet M. Clock-directed modular code generation for synchronous data-flow languages. ACM SIGPLAN Notices, 2008, 43(7): 121\u2013130","journal-title":"ACM SIGPLAN Notices"},{"key":"3910_CR30","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/978-3-642-30729-4_9","volume":"7321","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. Lecture Notes in Computer Science, 2012, 7321:113\u2013127","journal-title":"Lecture Notes in Computer Science"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-3910-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-013-3910-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-3910-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T21:01:18Z","timestamp":1559422878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-013-3910-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,13]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["3910"],"URL":"https:\/\/doi.org\/10.1007\/s11704-013-3910-8","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,13]]}}}