{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:38:16Z","timestamp":1725536296681},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_33","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"485-499","source":"Crossref","is-referenced-by-count":1,"title":["Liveness Reasoning with Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Jinshuang","family":"Wang","sequence":"first","affiliation":[]},{"given":"Huabing","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Xingyuan","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1-2","key":"33_CR1","doi-asserted-by":"publisher","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security\u00a06(1-2), 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"issue":"3","key":"33_CR2","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L.C. Paulson","year":"1999","unstructured":"Paulson, L.C.: Inductive analysis of the Internet protocol TLS. ACM Transactions on Computer and System Security\u00a02(3), 332\u2013351 (1999)","journal-title":"ACM Transactions on Computer and System Security"},{"issue":"1","key":"33_CR3","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci.\u00a083(1), 91\u2013130 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"33_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Information and Computation\u00a0103(1), 1\u201329 (1993)","journal-title":"Information and Computation"},{"issue":"2","key":"33_CR5","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/S0020-0190(98)00038-6","volume":"66","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: On the verification of qualitative properties of probabilistic processes under fairness constraints. Information Processing Letters\u00a066(2), 71\u201379 (1998)","journal-title":"Information Processing Letters"},{"key":"33_CR6","unstructured":"Jaeger, M.: Fairness, computable fairness and randomness. In: Proc. 2nd International Workshop on Probabilistic Methods in Verification (1999)"},{"key":"33_CR7","unstructured":"Yang, H., Zhang, X., Wang, Y.: Liveness proof of an elevator control system. In: The \u2018Emerging Trend\u2019 of TPHOLs, Oxford University Computing Lab. PRG-RR-05-02, pp. 190\u2013204 (2005)"},{"key":"33_CR8","unstructured":"Yang, H., Zhang, X., Wang, Y.: A correctness proof of the srp protocol. In: 20th International Parallel and Distributed Processing Symposium (IPDPS 2006), Proceedings, Rhodes Island, Greece, April 25-29 (2006)"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/11943952_7","volume-title":"Mobile Ad-hoc and Sensor Networks","author":"H. Yang","year":"2006","unstructured":"Yang, H., Zhang, X., Wang, Y.: A correctness proof of the dsr protocol. In: Cao, J., Stojmenovic, I., Jia, X., Das, S.K. (eds.) MSN 2006. LNCS, vol.\u00a04325, pp. 72\u201383. Springer, Heidelberg (2006)"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","author":"M. Wenzel","year":"2002","unstructured":"Wenzel, M.: Isar - a generic interpretative approach to readable formal proof documents. In: Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.) Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"33_CR12","first-page":"278","volume-title":"Proceedings of the fifteenth annual ACM symposium on Theory of computing","author":"A. Pnueli","year":"1983","unstructured":"Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: Proceedings of the fifteenth annual ACM symposium on Theory of computing, pp. 278\u2013290. ACM Press, New York (1983)"},{"key":"33_CR13","unstructured":"Zhang, X., Yang, H., Wang, Y.: Liveness reasoning for inductive protocol verification. In: The \u2018Emerging Trend\u2019 of TPHOLs, Oxford University Computing Lab. PRG-RR-05-02, pp. 221\u2013235 (2005)"},{"key":"33_CR14","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D thesis, University of Cambridge (2002)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-30142-4_20","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Richter","year":"2004","unstructured":"Richter, S.: Formlizing integration theory with an application to probabilistic algorithms. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 271\u2013286. Springer, Heidelberg (2004)"},{"key":"33_CR16","first-page":"278","volume-title":"Proceedings of the 15th annual ACM Symposium on Theory of Computing, Boston, Massachusetts","author":"A. Pnueli","year":"1983","unstructured":"Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: ACM (ed.) Proceedings of the 15th annual ACM Symposium on Theory of Computing, Boston, Massachusetts, April 25\u201327, pp. 278\u2013290. ACM Press, New York (1983)"},{"key":"33_CR17","unstructured":"Wang, J., Zhang, X., Zhang, Y., Yang, H.: A probabilistic model for parametric fairness in isabelle\/hol. Technical Report 364\/07, Department of Computer Science, University of Kaiserslautern (2007)"}],"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\/978-3-642-03359-9_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:42:57Z","timestamp":1552120977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}