{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:41Z","timestamp":1725551741661},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297970"},{"type":"electronic","value":"9783540322504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11576280_15","type":"book-chapter","created":{"date-parts":[[2005,10,24]],"date-time":"2005-10-24T14:01:26Z","timestamp":1130162486000},"page":"204-218","source":"Crossref","is-referenced-by-count":9,"title":["Jahuel: A Formal Framework for Software Synthesis"],"prefix":"10.1007","author":[{"given":"I.","family":"Assayad","sequence":"first","affiliation":[]},{"given":"V.","family":"Bertin","sequence":"additional","affiliation":[]},{"given":"F. -X.","family":"Defaut","sequence":"additional","affiliation":[]},{"given":"Ph.","family":"Gerner","sequence":"additional","affiliation":[]},{"given":"O.","family":"Qu\u00e9vreux","sequence":"additional","affiliation":[]},{"given":"S.","family":"Yovine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","volume-title":"DFMA 2005","author":"I. Assayad","year":"2005","unstructured":"Assayad, I., Gerner, P., Yovine, S., Bertin, V.: Modelling, analysis and implementation of an on-line video encoder. In: DFMA 2005, IEEE Computer Society, Los Alamitos (2005)"},{"key":"15_CR2","unstructured":"Inf. tech - Coding of audio-visual objects - P. 2: Visual. Prentice Hall, ISO\/IEC 14496-2:2001"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45828-X_28","volume-title":"Embedded Software","author":"V. Bertin","year":"2002","unstructured":"Bertin, V., Daveau, J.M., Guillaume, P., Lepley, T., Pilat, D., Richard, C., Santana, M., Thery, T.: FlexCC2: An optimizing retargetable C compiler for DSP proc. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol.\u00a02491. Springer, Heidelberg (2002)"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45449-7_31","volume-title":"Embedded Software","author":"P. Binns","year":"2001","unstructured":"Binns, P., Vestal, S.: Formalizing software architectures for embedded systems. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, p. 451. Springer, Heidelberg (2001)"},{"key":"15_CR5","volume-title":"Concurrency in Ada","author":"A. Burns","year":"1998","unstructured":"Burns, A., Wellings, A.: Concurrency in Ada. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR6","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 distrib. embedded applications. In: LCTES 2003 (2003)","DOI":"10.1145\/780732.780754"},{"key":"15_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1362-8","volume-title":"Scheduling and Automatic Parallelization","author":"A. Darte","year":"2000","unstructured":"Darte, A., Robert, Y., Vivien, F.: Scheduling and Automatic Parallelization. Birkh\u00e4user, Boston (2000)"},{"key":"15_CR8","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1188.001.0001","volume-title":"Algebraic Semantics of Imperative Programs","author":"J. Goguen","year":"1996","unstructured":"Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)"},{"key":"15_CR9","unstructured":"Goguen, J., Wang, G., Nam, Y.-K., Lin, K.: Abstract schema morphisms and schema matching generation. Tech. Rep. DCSE, UCSD (2004)"},{"key":"15_CR10","volume-title":"Using MPI. Scientific and Engineering Computation","author":"W. Groppa","year":"1999","unstructured":"Groppa, W., Lusk, E., Skjellum, A.: Using MPI. Scientific and Engineering Computation, 2nd edn. MIT Press, Cambridge (1999)","edition":"2"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. In: Proc. IEEE, vol.\u00a079(9) (September 1991)","DOI":"10.1109\/5.97300"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Hammond, L., Nayfeh, B.A., Olukotun, K.: A single-chip multiprocessor. Comp.\u00a030(9) (1997)","DOI":"10.1109\/2.612253"},{"key":"15_CR13","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Karsai, G., Sztipanovits, J., Ledeczi, A., Bapty, T.: Model-integrated development of embedded software. In: Proc. IEEE, vol.\u00a091(1) (2003)","DOI":"10.1109\/JPROC.2002.805824"},{"key":"15_CR15","unstructured":"Kersten, M.: Comparison of the leading AOP tools. In: Aspect-Oriented Software Development, AOSD 2005 (2005) Industry track. Invited talk"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45212-6_18","volume-title":"Embedded Software","author":"C. Kloukinas","year":"2003","unstructured":"Kloukinas, C., Nakhli, C., Yovine, S.: A Methodology and Tool Support for Generating Scheduled Native Code for Real-Time Java Applications. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol.\u00a02855, pp. 274\u2013289. Springer, Heidelberg (2003)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Kloukinas, C., Yovine, S.: Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems. In: ECRTS 2003 (2003)","DOI":"10.1109\/EMRTS.2003.1212754"},{"key":"15_CR18","unstructured":"http:\/\/www.openmp.org"},{"key":"15_CR19","unstructured":"http:\/\/ptolemy.eecs.berkeley.edu\/ptolemyII"},{"key":"15_CR20","unstructured":"Sangiovanni-Vincentelli, A.: Defining platform-based design. EEDesign, February 5 (2002)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Schlett, M.: Trends in embedded-microprocessor design. IEEE Computer\u00a031(8) (1998)","DOI":"10.1109\/2.707616"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/3-540-45449-7_26","volume-title":"Embedded Software","author":"J. Sifakis","year":"2001","unstructured":"Sifakis, J.: Modeling real-time systems - challenges and work directions. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol.\u00a02211, p. 373. Springer, Heidelberg (2001)"},{"issue":"1","key":"15_CR23","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/JPROC.2002.805820","volume":"91","author":"J. Sifakis","year":"2003","unstructured":"Sifakis, J., Tripakis, S., Yovine, S.: Building models of real-time systems from application software. Proceedings of the IEEE\u00a091(1), 100\u2013111 (2003)","journal-title":"Proceedings of the IEEE"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11576280_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:59:31Z","timestamp":1605643171000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11576280_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297970","9783540322504"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11576280_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}