{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T18:40:14Z","timestamp":1743619214913,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642307287"},{"type":"electronic","value":"9783642307294"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30729-4_9","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:49:46Z","timestamp":1340786986000},"page":"113-127","source":"Crossref","is-referenced-by-count":9,"title":["Formal Verification of Compiler Transformations on Polychronous Equations"],"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":[]},{"given":"Lo\u00efc","family":"Besnard","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"9_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Le Borgne, M., Benveniste, A., Le Guernic, P.: Dynamical systems over Galois fields and control problems. In: Proceedings of 33th IEEE on Decision and Control, vol.\u00a03, pp. 1505\u20131509 (1991)","DOI":"10.1109\/CDC.1991.261653"},{"key":"9_CR3","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"},{"key":"9_CR4","unstructured":"Besnard, L., Gautier, T., Moy, M., Talpin, J.-P., Johnson, K., Maraninchi, F.: Automatic translation of C\/C++ parallel code into synchronous formalism using an SSA intermediate form. In: Proceedings of the 9th Workshop on Automated Verification of Critical Systems, AVOCS (2009)"},{"key":"9_CR5","unstructured":"Dutertre, B., Le Borgne, M., Marchand, H.: SIGALI: un syst\u00e8me de calcul formel pour la v\u00e9rification de programmes SIGNAL. Manuel d\u2019utilisation. Note technique, non publi\u00e9e (December 1998)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"9_CR7","volume-title":"Designing embedded systems with the SIGNAL programming: Synchronous, Reactive Specification","author":"A. Gamatie","year":"2009","unstructured":"Gamatie, A.: Designing embedded systems with the SIGNAL programming: Synchronous, Reactive Specification. Springer, New York (2009) ISBN 978-1-4419-0940-4"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1142\/S0218126603000763","volume":"12","author":"P. Guernic Le","year":"2003","unstructured":"Le Guernic, P., Talpin, J.-P., Le Lann, J.-C.: Polychrony for system design. Journal for Circuits, Systems and Computers\u00a012(3), 261\u2013304 (2003)","journal-title":"Journal for Circuits, Systems and Computers"},{"key":"9_CR9","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":"9_CR10","doi-asserted-by":"crossref","unstructured":"Kouchnarenko, O., Pinchinat, S.: Intensional approaches for symbolic methods. Electronic Notes in Theoretical Computer Science (August 1998)","DOI":"10.1016\/S1571-0661(05)80253-1"},{"issue":"1","key":"9_CR11","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0167-6423(00)00020-4","volume":"41","author":"H. Marchand","year":"2001","unstructured":"Marchand, H., Rutten, H., Le Borgne, E., Samaan, M.: Formal verification of SIGNAL programs: Application to a power transformer station controller. Science of Computer Programming\u00a041(1), 85\u2013104 (2001)","journal-title":"Science of Computer Programming"},{"key":"9_CR12","unstructured":"Polychrony Toolset, http:\/\/www.irisa.fr\/espresso\/Polychrony\/"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Peralta, J.C., Gautier, T., Besnard, L., Le Guernic, P.: LTSs for translation validation of (multi-clocked) SIGNAL specifications. In: 8th IEEE\/ACM International Conference on Formal Method and Models for Codesign, MEMOCODE (2010)","DOI":"10.1109\/MEMCOD.2010.5558632"},{"key":"9_CR14","unstructured":"Pinchinat, S., Marchand, H., Le Borgne, M.: Symbolic abstractions of automata and their application to the supervisory control problem. In: INRIA Technical Reports No 1279, pp. 1\u201329 (November 1999)"},{"key":"9_CR15","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.D.: 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":"9_CR16","unstructured":"Milner, R.: Operational and algebraic semantics of concurrent processes. Research Report ECS-LFCS-88-46, Lab. for Foundations of Computer Science, Edinburgh (February 1988)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-57208-2_6","volume-title":"CONCUR\u201993","author":"R.J. Glabbeek Van","year":"1993","unstructured":"Van Glabbeek, R.J.: The Linear Time-Branching Time Spectrum II: The Semantics of Sequential Systems with Silent Moves (Extended Abstract). In: Best, E. (ed.) CONCUR 1993. LNCS, vol.\u00a0715, pp. 66\u201381. Springer, Heidelberg (1993)"},{"key":"9_CR18","unstructured":"VeriSync Project, http:\/\/www.irit.fr\/Verisync\/"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30729-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T18:21:20Z","timestamp":1743618080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30729-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642307287","9783642307294"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30729-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}