{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T11:05:35Z","timestamp":1767611135145},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642244308"},{"type":"electronic","value":"9783642244315"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24431-5_16","type":"book-chapter","created":{"date-parts":[[2011,8,24]],"date-time":"2011-08-24T02:29:46Z","timestamp":1314152986000},"page":"212-227","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Real-Time Data Processing of the LHC Beam Loss Monitoring System: A Case Study"],"prefix":"10.1007","author":[{"given":"Naghmeh","family":"Ghafari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeff","family":"Joyce","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Dehning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christos","family":"Zamantzas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Arthan, R.: ProofPower manuals (2004), http:\/\/lemma-one.com\/ProofPower\/index\/index.html"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. J. Symb. Log.\u00a05(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"16_CR3","unstructured":"Coquand, T., Huet, G.: Coq manuals (2010), http:\/\/coq.inria.fr"},{"key":"16_CR4","unstructured":"Dehning, B.: Beam loss monitoring system for machine protection. In: Proceedings of DIPAC, pp. 117\u2013121 (2005)"},{"key":"16_CR5","unstructured":"Harrison, J.: HOL Light manuals (2010), http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Milner, R.: Logic for Computable Functions: Description of a Machine Implementation. Technical report, Stanford, CA, USA (1972)","DOI":"10.21236\/AD0785072"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1109\/VIUF.1997.623934","volume":"0","author":"R. Nair","year":"1997","unstructured":"Nair, R., Ryan, G., Farzaneh, F.: A Symbol Based Algorithm for Hardware Implementation of Cyclic Redundancy Check (CRC). VHDL International User\u2019s Forum\u00a00, 82 (1997)","journal-title":"VHDL International User\u2019s Forum"},{"key":"16_CR8","unstructured":"Norrish, M., Slind, K.: HOL4 manuals (1998), http:\/\/hol.sourceforge.net"},{"key":"16_CR9","unstructured":"Owre, S., Shankar, N., Rushby, J., Stringer-Calvert, D.: PVS manuals (2010), http:\/\/pvs.csl.sri.com"},{"key":"16_CR10","unstructured":"Paulson, L., Nipkow, T., Wenzel, M.: Isabelle manuals (2009), http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html"},{"key":"16_CR11","unstructured":"Rushby, J.: Formal Methods and the Certification of Critical systems. CSL Technical Report 93-7, SRI International (December 1993)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Schmidt, R., Assmann, R.W., Burkhardt, H., Carlier, E., Dehning, B., Goddard, B., Jeanneret, J.B., Kain, V., Puccio, B., Wenninger, J.: Beam Loss Scenarios and Strategies for Machine Protection at the LHC. In: Proceedings of HALO, pp. 184\u2013187 (2003)","DOI":"10.1063\/1.1638351"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A Brief Overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1147\/rd.275.0440","volume":"27","author":"A.X. Widmer","year":"1983","unstructured":"Widmer, A.X., Franaszek, P.A.: A DC-balanced, partitioned-block, 8B\/10B transmission code. IBM J. Res. Dev.\u00a027, 440\u2013451 (1983)","journal-title":"IBM J. Res. Dev."},{"key":"16_CR15","unstructured":"Zamantzas, C.: The Real-Time Data Analysis and Decision System for Particle Flux Detection in the LHC Accelerator at CERN. Ph.D. Thesis, Brunel University (2006)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Zamantzas, C., Dehning, B., Effinger, E., Emery, J., Ferioli, G.: An FPGA Based Implementation for Real-Time Processing of the LHC Beam Loss Monitoring System\u2019s Data. In: IEEE Nuclear Science Symposium Conference Record, pp. 950\u2013954 (2006)","DOI":"10.1109\/NSSMIC.2006.356003"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24431-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T09:34:01Z","timestamp":1560504841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24431-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642244308","9783642244315"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24431-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}