{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,29]],"date-time":"2025-12-29T22:18:25Z","timestamp":1767046705358,"version":"3.30.1"},"reference-count":32,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4946,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1016\/s0167-6423(99)00015-5","type":"journal-article","created":{"date-parts":[[2002,10,31]],"date-time":"2002-10-31T21:12:04Z","timestamp":1036098724000},"page":"5-25","source":"Crossref","is-referenced-by-count":34,"title":["ESTEREL: a formal method applied to avionic software development"],"prefix":"10.1016","volume":"36","author":[{"given":"G\u00e9rard","family":"Berry","sequence":"first","affiliation":[]},{"given":"Amar","family":"Bouali","sequence":"additional","affiliation":[]},{"given":"Xavier","family":"Fornari","sequence":"additional","affiliation":[]},{"given":"Emmanuel","family":"Ledinot","sequence":"additional","affiliation":[]},{"given":"Eric","family":"Nassor","sequence":"additional","affiliation":[]},{"given":"Robert","family":"de Simone","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(99)00015-5_BIB1","doi-asserted-by":"crossref","unstructured":"J.R. Abrial, M.K.O. Lee, D.S. Neilson, P.N. Scharbach, I.H. S\u00f8rensen, The B-method, in: VDM\u201991: Formal Software Development Methods, Vol. 2, Lecture notes in Computer Science, vol. 552, Springer, Berlin, 1991, pp. 398\u2013405.","DOI":"10.1007\/BFb0020001"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB2","unstructured":"C. Andre, Representation and analysis of reactive behaviors: a synchronous approach, in: Computational Engineering in Systems Applications, Lille (France), (1996) IEEE-SMC pp. 19\u201329."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB3","unstructured":"C. Andr\u00e9, M. Bourdell\u00e8s, S. Dissoubray, SYNCCHARTS\/ESTEREL: un environnement graphique pour la sp\u00e9cification et la programmation d'applications r\u00e9actives complexes, Rev. du G\u00e9nie Logiciel 46 (1997)."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1098\/rsta.1992.0027","article-title":"Esterel on hardware","volume":"339","author":"Berry","year":"1992","journal-title":"Philos. Trans. Roy. Soc. London A"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB5","unstructured":"G. Berry. The Constructive Semantics of Esterel, Draft book available at: http:\/\/www.inria.fr\/meije\/esterel, 1998."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB6","unstructured":"G. Berry, The Foundations of Esterel, in: G. Plotkin, C. Stirling, M. Tofte (Eds.), Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, MA, 1998, to appear."},{"issue":"2","key":"10.1016\/S0167-6423(99)00015-5_BIB7","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","article-title":"The Esterel synchronous programming language: design, semantics, implementation","volume":"19","author":"Berry","year":"1992","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB8","doi-asserted-by":"crossref","unstructured":"A. Bouali, XEVE, an Esterel Verification Environment, in: Proc. Tenth Int. Conf. on Computer Aided Verification CAV\u201998, Lecture Notes in Computer Science, UBC, Vancouver, Canada, June 1998.","DOI":"10.1007\/BFb0028770"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB9","doi-asserted-by":"crossref","unstructured":"A. Bouali, J.-P. Marmorat, R. De Simone, H. Toma, Verifying Synchronous Reactive Systems Programmed in Esterel, Lecture Notes in Computer Science, Vol. 1135, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61648-9_57"},{"issue":"6","key":"10.1016\/S0167-6423(99)00015-5_BIB10","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/173262.155095","article-title":"Abstract debugging of higher-order imperative languages","volume":"28","author":"Bourdoncle","year":"1993","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB11","doi-asserted-by":"crossref","unstructured":"F. Bourdoncle, Efficient chaotic iteration strategies with widenings, Lecture Notes in Computer Science, Vol. 735, Springer, Berlin, 1993.","DOI":"10.1007\/BFb0039704"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB12","doi-asserted-by":"crossref","first-page":"1293","DOI":"10.1109\/5.97299","article-title":"The Esterel language, Another Look at Real Time Programming","volume":"79","author":"Boussinot","year":"1991","journal-title":"Proc. IEEE"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB13","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean function manipulation","volume":"C-35(8)","author":"Bryant","year":"1986","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB14","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, L. McMillan, D.L. Dill, J. Hwang, Symbolic model checking: 1020 and beyond, in: 5th IEEE Symp. on Logic in Computer Science, Philadelphia, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB15","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, K.L. McMillan, Compositional model checking, in: Proc. Fourth Ann. Symp. on Logic in Computer Science, Pacific Grove, CA, IEEE Computer Society Press, Silver Spring, MD, 5\u20138 June 1989, pp. 353\u2013362.","DOI":"10.1109\/LICS.1989.39190"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB16","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. Comput."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB17","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J.C. Madre, Verification of synchronous sequential machines based on symbolic execution, in: Automatic Verification Methods For Finite State Systems, Grenoble, France, Lecture Notes in Computer Science, Vol. 407, Springer, Berlin, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB18","unstructured":"O. Coudert, J.-C. Madre, H. Touati, TiGeR Version 1.0 User Guide, Digital Paris Research Lab, December 1993."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB19","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer, Dordrecht, 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB20","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, P. Raymond, Synchronous observers and the verification of reactive systems, in: Proc. 3rd Int. Conf. on Algebraic Methodology and Software Technology, AMAST\u201993, Workshops in Computing, Springer, Berlin, June 1993.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"issue":"3","key":"10.1016\/S0167-6423(99)00015-5_BIB21","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","article-title":"Statecharts: a visual formalism for complex systems","volume":"8","author":"Harel","year":"1987","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB22","doi-asserted-by":"crossref","unstructured":"L. Holenderski, A. Poign\u00e9, Synchronie workbench, in: Proc. ATOOLS\u201998 Workshop on Analysis Tool Support for System Specification, Development and Verification, Malente, Germany, June 1998.","DOI":"10.1007\/978-3-7091-6355-9_9"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB23","doi-asserted-by":"crossref","unstructured":"L.J. Jagadeesan, C. Puchol, J. Von Olnhausen, Safety property verification of Esterel programs and application to telecommunications software, in: Computer-Aided Verification, Lecture Notes in Computer Science, vol. 939, Liege, Belgium, July 1995.","DOI":"10.1007\/3-540-60045-0_45"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB24","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking, Lecture Notes in Computer Science, Vol. 1427, Springer, Berlin, 1998.","DOI":"10.1007\/BFb0028738"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB25","doi-asserted-by":"crossref","unstructured":"J. Misra, K. Mani Chandy, Proofs of networks of processes, IEEE Trans. Software Engng. 7 (4) (1981) 417\u2013426.","DOI":"10.1109\/TSE.1981.230844"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB26","doi-asserted-by":"crossref","unstructured":"S. Malik, Analysis of cyclic combinational circuits, in: IEEE\/ACM Int. Conf. on CAD, Santa Clara, CA, ACM\/IEEE, IEEE Computer Society Press, Silver Spring, MD, November 1993, pp. 618\u2013627.","DOI":"10.1109\/ICCAD.1993.580150"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB27","doi-asserted-by":"crossref","unstructured":"E.M. Sentovich, K.J. Singh, L. Lavagno, C. Moon, R. Murgai, A. Saldanha, H. Savoj, P.R. Stephan, R.K. Brayton, A.Sangiovanni-Vincentelli, SIS: a system for sequential circuit synthesis, Technical Report, U.C. Berkeley, May 1992.","DOI":"10.1109\/ICCD.1992.276282"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB28","doi-asserted-by":"crossref","unstructured":"E.M. Sentovich, H. Toma, G. Berry, Latch optimization in circuits generated from high-level descriptions, Proc. IEEE\/ACM Internat. Conf. on Computer-Aided Design, November 1996.","DOI":"10.1109\/ICCAD.1996.569833"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB29","doi-asserted-by":"crossref","unstructured":"H. Sentovich, H. Toma, G. Berry, Efficient latch optimization using incompatible sets, Proc. 34th Des. Automat. Conf., June 1997.","DOI":"10.1109\/DAC.1997.597108"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB30","doi-asserted-by":"crossref","unstructured":"T. Shiple, G. Berry, H. Touati, Constructive analysis of cyclic circuits, Proc. Int. Des. Testing Conf. (ITDC), Paris, 1996.","DOI":"10.1109\/EDTC.1996.494321"},{"key":"10.1016\/S0167-6423(99)00015-5_BIB31","unstructured":"Esterel Team, The Esterel v5 Language Primer, Ecole des Mines\/INRIA, available at http:\/\/www.inria.fr\/meije\/esterel\/, Esterel Compiler Documentation, 1998."},{"key":"10.1016\/S0167-6423(99)00015-5_BIB32","unstructured":"H. Toma, Analyse constructive et optimisation s\u00e9quentielle des circuits g\u00e9n\u00e9r\u00e9s \u00e0 partir du langage synchrone r\u00e9actif ESTEREL, Ph.D. Thesis, \u00c9cole des Mines de Paris, 1997 (in French)."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642399000155?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642399000155?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,6]],"date-time":"2024-12-06T06:26:49Z","timestamp":1733466409000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642399000155"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["S0167642399000155"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(99)00015-5","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}