{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:48:32Z","timestamp":1725540512035},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_26","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T11:45:27Z","timestamp":1258371927000},"page":"504-520","source":"Crossref","is-referenced-by-count":9,"title":["Proof Assisted Model Checking for B"],"prefix":"10.1007","author":[{"given":"Jens","family":"Bendisposto","sequence":"first","affiliation":[]},{"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/11901433_32","volume-title":"Formal Methods and Software Engineering","author":"J.-R. Abrial","year":"2006","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S.: An open extensible tool environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 588\u2013605. Springer, Heidelberg (2006)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: Modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-24771-5_3","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"K. Arkoudas","year":"2004","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.C.: Integrating model checking and theorem proving for relational reasoning. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol.\u00a03051, pp. 21\u201333. Springer, Heidelberg (2004)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","first-page":"87","volume-title":"FOSSACS 2003","author":"T. Arons","year":"2003","unstructured":"Arons, T., Pnueli, A., Zuck, L.: Parameterized verification by probabilistic abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 87\u2013102. Springer, Heidelberg (2003)"},{"key":"26_CR6","unstructured":"Bendisposto, J., Jastram, M., Leuschel, M., Lochert, C., Scheuermann, B., Weigelt, I.: Validating Wireless Congestion Control and Realiability Protocols using ProB and Rodin. FMWS 2008: Workshop on Formal Methods for Wireless Systems (August 2008)"},{"issue":"8","key":"26_CR7","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.3166\/tsi.27.1065-1084","volume":"27","author":"J. Bendisposto","year":"2008","unstructured":"Bendisposto, J., Leuschel, M., Ligot, O., Samia, M.: La validation de mod\u00e8les event-b avec le plug-in prob pour rodin. Technique et Science Informatiques\u00a027(8), 1065\u20131084 (2008)","journal-title":"Technique et Science Informatiques"},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s00165-007-0061-4","volume":"20","author":"M. Butler","year":"2008","unstructured":"Butler, M., Yadav, D.: An incremental development of the Mondex system in Event-B. Formal Aspects of Computing\u00a020(1), 61\u201377 (2008)","journal-title":"Formal Aspects of Computing"},{"key":"26_CR9","volume-title":"UML-B Specification for Proven Embedded Systems Design, ch. 16","author":"D. Cansell","year":"2004","unstructured":"Cansell, D., Hallerstede, S., Oliver, I.: UML-B specification and hardware implementation of a hamming coder\/decoder. In: Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design, ch. 16, November 2004. Kluwer Academic Publishers, Dordrecht (2004)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Hiraishi, H., Jha, S.: Verification of the futurebus+ cache coherence protocol. Formal Methods in System Design (January 1995)","DOI":"10.1007\/BF01383968"},{"key":"#cr-split#-26_CR11.1","unstructured":"Dams, D., Hutter, D., Sidorova, N.: Using the inka prover to automate safety proofs in abstract interpretation - a case study. In: Bellegarde, F., Kouchnarenko, O. (eds.) Workshop on Modelling and Verification, C.I.S., Besan\u00e7on, France (1999);"},{"key":"#cr-split#-26_CR11.2","unstructured":"Alternative title: Combining Theorem Proving and Model Checking - A Case Study"},{"issue":"15","key":"26_CR12","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.1016\/j.infsof.2004.07.002","volume":"46","author":"P. Dybjer","year":"2004","unstructured":"Dybjer, P., Haiyan, Q., Takeyama, M.: Verifying haskell programs by combining testing, model checking and interactive theorem proving. Information & Software Technology\u00a046(15), 1011\u20131025 (2004)","journal-title":"Information & Software Technology"},{"key":"26_CR13","unstructured":"Freitas, L.: Model Checking Circus. PhD thesis, University of York (2005)"},{"issue":"1","key":"26_CR14","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s11334-006-0021-9","volume":"2","author":"L. Freitas","year":"2006","unstructured":"Freitas, L., Woodcock, J., Cavalcanti, A.: State-rich model checking. Innovations Syst. Softw. Eng.\u00a02(1), 49\u201364 (2006)","journal-title":"Innovations Syst. Softw. Eng."},{"issue":"2","key":"26_CR15","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/s00165-005-0059-8","volume":"17","author":"E.L. Gunter","year":"2005","unstructured":"Gunter, E.L., Peled, D.: Model checking, testing and verification working together. Formal Asp. Comput.\u00a017(2), 201\u2013221 (2005)","journal-title":"Formal Asp. Comput."},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/3-540-45614-7_2","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"B. Legeard","year":"2002","unstructured":"Legeard, B., Peureux, F., Utting, M.: Automated boundary testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 21\u201340. Springer, Heidelberg (2002)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-87603-8_2","volume-title":"Abstract State Machines, B and Z","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M.: The high road to formal validation. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 4\u201323. Springer, Heidelberg (2008)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"issue":"2","key":"26_CR19","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT\u00a010(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"708","DOI":"10.1007\/978-3-642-05089-3_45","volume-title":"Proceedings FM 2009","author":"M. Leuschel","year":"2009","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale b models. In: Cavalcanti, A., Dams, D. (eds.) Proceedings FM 2009. LNCS, vol.\u00a05850, pp. 708\u2013723. Springer, Heidelberg (2009)"},{"key":"26_CR21","unstructured":"Leuschel, M., Plagge, D.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. In: Ameur, Y.A., Boniol, F., Wiels, V. (eds.) Proceedings Isola 2007, C\u00e9padu\u00e8s edn. Revue des Nouvelles Technologies de l\u2019Information, vol.\u00a0RNTI-SM-1, pp. 73\u201384 (2007)"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-60580-0","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. M\u00fcller","year":"1995","unstructured":"M\u00fcller, O., Nipkow, T.: Combining model checking and deduction for i\/o-automata. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 1\u201316. Springer, Heidelberg (1995)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1996","unstructured":"Pnueli, A., Shahar, E.: A platform for combining deductive with algorithmic verification. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 184\u2013195. Springer, Heidelberg (1996)"},{"key":"26_CR26","first-page":"40","volume":"65","author":"A. Romanovsky","year":"2006","unstructured":"Romanovsky, A.: Rigorous Open Development Environment for Complex Systems - RODIN. ERCIM News\u00a065, 40\u201341 (2006)","journal-title":"ERCIM News"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Scheuermann, B., Lochert, C., Mauve, M.: Implicit hop-by-hop congestion control in wireless multihop networks. In: Ad Hoc Networks (2007), doi:10.1016\/j.adhoc.2007.01.001","DOI":"10.1016\/j.adhoc.2007.01.001"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44618-4_1","volume-title":"CONCUR 2000 - Concurrency Theory","author":"N. Shankar","year":"2000","unstructured":"Shankar, N.: Combining theorem proving and model checking through symbolic analysis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 1\u201316. Springer, Heidelberg (2000)"},{"issue":"1","key":"26_CR29","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1008791913551","volume":"15","author":"H. Sipma","year":"1999","unstructured":"Sipma, H., Uribe, T., Manna, Z.: Deductive model checking. Formal Methods in System Design\u00a015(1), 49\u201374 (1999)","journal-title":"Formal Methods in System Design"},{"key":"26_CR30","first-page":"15","volume-title":"Proceedings Symposium TASE 2008","author":"C. Spermann","year":"2008","unstructured":"Spermann, C., Leuschel, M.: ProB gets nauty: Effective symmetry reduction for B and Z models. In: Proceedings Symposium TASE 2008, Nanjing, China, pp. 15\u201322. IEEE, Los Alamitos (2008)"},{"key":"26_CR31","unstructured":"Steria, F.: Aix-en-Provence. In: Atelier B, User and Reference Manuals (1996), http:\/\/www.atelierb.societe.com"},{"key":"26_CR32","series-title":"LNAI","first-page":"151","volume-title":"Frocos 2000","author":"T. Uribe","year":"2000","unstructured":"Uribe, T.: Combinations of model checking and theorem proving. In: Kirchner, H., Ringeissen, C. (eds.) Frocos 2000. LNCS (LNAI), vol.\u00a01794, pp. 151\u2013170. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:54:55Z","timestamp":1606186495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}