{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:37Z","timestamp":1725487777753},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_22","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T13:40:26Z","timestamp":1185025226000},"page":"356-371","source":"Crossref","is-referenced-by-count":3,"title":["Specification and Verification of a Steam-Boiler with Signal-Coq"],"prefix":"10.1007","author":[{"given":"Micka\u00ebl","family":"Kerb\u0153uf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Nowak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"J.-R. Abrial. The B-Book. Cambridge University Press, 1995."},{"key":"22_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027227","volume-title":"Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control","author":"J.-R. Abrial","year":"1996","unstructured":"J.-R. Abrial, E. B\u00f6rger, and H. Langmaack. Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. Lecture Notes in Computer Science, 1165, October 1996."},{"key":"22_CR3","unstructured":"S. Bensalem, P. Caspi, and C. Parent-Vigouroux. Handling Data-flow Programs in PVS. Research report (draft), Verimag, May 1996."},{"issue":"2","key":"22_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(91)90001-E","volume":"16","author":"A. Benveniste","year":"1991","unstructured":"A. Benveniste and P. Le Guernic. Synchronous Programming with Events and Relations: the SIGNAL Language and its Semantics. Science of Computer Programming, 16(2): 103\u2013149, 1991.","journal-title":"Science of Computer Programming"},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Gonthier. The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming, 19:87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"22_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/BFb0027235","volume-title":"The Steam-Boiler Problem in Lustre","author":"T. Cattel","year":"1996","unstructured":"T. Cattel and G. Duval. The Steam-Boiler Problem in Lustre. Lecture Notes in Computer Science, 1165:149\u2013164, 1996."},{"key":"22_CR7","volume-title":"The Coq Proof Assistant Reference Manual-Version 6.2","author":"B. Barras","year":"1998","unstructured":"B. Barras et al. The Coq Proof Assistant Reference Manual-Version 6.2. INRIA, Rocquencourt, May 1998."},{"key":"22_CR8","unstructured":"E Gim\u00e9nez. Un Calcul de Constructions Infinies et son Application \u00e0 la V\u00e9rification des Syst\u00e8mes Communicants. PhD thesis, Laboratoire de l\u2019Informatique du Parall\u00e9lisme, Ecole Normale Sup\u00e9rieure de Lyon, December 1996."},{"issue":"9","key":"22_CR9","doi-asserted-by":"publisher","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The Synchronous Dataflow Programming Language Lustre. Proc. of the IEEE, 79(9): 1305\u20131320, September 1991.","journal-title":"Proc. of the IEEE"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"22_CR11","series-title":"Research Report","volume-title":"The Steam-boiler Controller Problem in Signal-Coq","author":"M. Kerbosuf","year":"1999","unstructured":"M. Kerbosuf, D. Nowak, and J.-P. Talpin. The Steam-boiler Controller Problem in Signal-Coq. Research Report 3773, INRIA, Campus universitaire de Beaulieu, 35042 RENNES Cedex (France), October 1999."},{"key":"22_CR12","unstructured":"http:\/\/www.irisa.fr\/prive\/Mickael.Kerboeuf\/gb\/SBGB.htm\n                  \n                ."},{"key":"22_CR13","unstructured":"D. Nowak. Sp\u00e9cification et preuve de syst\u00e8mes r\u00e9actifs. PhD thesis, Ifsic, Univer-sit\u00e9 Rennes I, October 1999."},{"key":"22_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/BFb0055148","volume-title":"Proceedings of Theorem Proving in Higher Order Logics (TPHOLs\u201998)","author":"D. Nowak","year":"1998","unstructured":"D. Nowak, J.-R. Beauvais, and J.-P. Talpin. Co-inductive Axiomatization of a Synchronous Language. In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs\u201998), number 1479 in LNCS, pages 387\u2013399. Springer Verlag, September 1998."},{"key":"22_CR15","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, Universit\u00e9 Paris VII, May 1994."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,18]],"date-time":"2019-02-18T02:01:32Z","timestamp":1550455292000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}