{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T03:12:51Z","timestamp":1743045171987,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929699"},{"type":"electronic","value":"9783319929705"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_15","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T08:54:12Z","timestamp":1527584052000},"page":"239-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[]},{"given":"Olga","family":"Grinchtein","sequence":"additional","affiliation":[]},{"given":"Justin","family":"Pearson","sequence":"additional","affiliation":[]},{"given":"Mats","family":"Carlsson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"15_CR1","unstructured":"3GPP. Public warning system (PWS) requirements. TS 22.268, 3rd Generation Partnership Project (3GPP). http:\/\/www.3gpp.org\/ftp\/Specs\/html-info\/22268.htm"},{"key":"15_CR2","unstructured":"Barras, B., Werner, B.: Coq in Coq. Technical report, INRIA-Rocquencourt (1997)"},{"issue":"1","key":"15_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-015-9336-2","volume":"56","author":"J Bengtson","year":"2016","unstructured":"Bengtson, J., Parrow, J., Weber, T.: Psi-Calculi in Isabelle. J. Autom. Reasoning 56(1), 1\u201347 (2016)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1007\/978-3-319-13560-1_63","volume-title":"PRICAI 2014: Trends in Artificial Intelligence","author":"C Bessiere","year":"2014","unstructured":"Bessiere, C., Hebrard, E., Katsirelos, G., Kiziltan, Z., Narodytska, N., Walsh, T.: Reasoning about Constraint Models. In: Pham, D.-N., Park, S.-B. (eds.) PRICAI 2014. LNCS (LNAI), vol. 8862, pp. 795\u2013808. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13560-1_63"},{"issue":"1","key":"15_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01212523","volume":"9","author":"M Bezem","year":"1997","unstructured":"Bezem, M., Bol, R., Groote, J.F.: Formalizing process algebraic verifications in the calculus of constructions. Formal Aspects Comput. 9(1), 1\u201348 (1997)","journal-title":"Formal Aspects Comput."},{"key":"15_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Workshop on Intermediate Verification Languages (2011)"},{"key":"15_CR7","unstructured":"Borgstr\u00f6m, J., Huang, S., Johansson, M., Raabjerg, P., Victor, B., Pohjola, J.\u00c5., Parrow, J.: Broadcast psi-calculi with an application to wireless protocols. Softw. Syst. Model. 14(1), 201\u2013216 (2015)"},{"issue":"4&5","key":"15_CR8","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1080\/08839510701252650","volume":"21","author":"M Cadoli","year":"2007","unstructured":"Cadoli, M., Mancini, T.: Using a theorem prover for reasoning on constraint problems. Appl. Artif. Intell. 21(4&5), 383\u2013404 (2007)","journal-title":"Appl. Artif. Intell."},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-61780-9_67","volume-title":"Types for Proofs and Programs","author":"E Gim\u00e9nez","year":"1996","unstructured":"Gim\u00e9nez, E.: An application of co-inductive types in Coq: verification of the alternating bit protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 135\u2013152. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61780-9_67"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: 8th Asian Symposium of Computer Mathematics, p. 333. ASCM (2007)","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-21215-9_9","volume-title":"Tests and Proofs","author":"O Grinchtein","year":"2015","unstructured":"Grinchtein, O., Carlsson, M., Pearson, J.: A constraint optimisation model for analysis of telecommunication protocol logs. In: Blanchette, J.C., Kosmatov, N. (eds.) TAP 2015. LNCS, vol. 9154, pp. 137\u2013154. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21215-9_9"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of $$\\mu $$CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes. Workshops in Computing. Springer, London (1995). https:\/\/doi.org\/10.1007\/978-1-4471-2120-6_2","DOI":"10.1007\/978-1-4471-2120-6_2"},{"issue":"1","key":"15_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-008-9105-6","volume":"42","author":"O Hasan","year":"2009","unstructured":"Hasan, O., Tahar, S.: Performance analysis and functional verification of the stop-and-wait protocol in HOL. J. Autom. Reason. 42(1), 1\u201333 (2009)","journal-title":"J. Autom. Reason."},{"issue":"7","key":"15_CR14","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1007\/978-3-540-74970-7_38","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"N Nethercote","year":"2007","unstructured":"Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G.: MiniZinc: towards a standard CP modelling language. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 529\u2013543. Springer, Heidelberg (2007)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"1","key":"15_CR17","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1109\/COMST.2014.2345792","volume":"17","author":"J Qadir","year":"2015","unstructured":"Qadir, J., Hasan, O.: Applying formal methods to networking: theory, techniques, and applications. IEEE Commun. Surv. Tutorials 17(1), 256\u2013291 (2015)","journal-title":"IEEE Commun. Surv. Tutorials"},{"volume-title":"Handbook of Constraint Programming","year":"2006","key":"15_CR18","unstructured":"Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming. Elsevier, New York (2006)"},{"issue":"3","key":"15_CR19","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/1015850.1015853","volume":"8","author":"CA Sunshine","year":"1978","unstructured":"Sunshine, C.A.: Survey of protocol definition and verification techniques. SIGCOMM Comput. Commun. Rev. 8(3), 35\u201341 (1978)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"15_CR20","unstructured":"The Coq Development Team. The Coq proof assistant reference manual version 8.6 (2016)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T15:23:55Z","timestamp":1571412235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}