{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:17Z","timestamp":1725558977894},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255598"},{"type":"electronic","value":"9783540320074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11415787_2","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:07:36Z","timestamp":1278886056000},"page":"6-23","source":"Crossref","is-referenced-by-count":16,"title":["Visualising Larger State Spaces in Pro B"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[]},{"given":"Edd","family":"Turner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"publisher","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":"2_CR2","volume-title":"Compilers \u2014 Principles, Techniques and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers \u2014 Principles, Techniques and Tools. Addison-Wesley, Reading (1986)"},{"key":"2_CR3","unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-testing-tools: A tool-set for test generation from Z and B using constraint logic programming. In: Proceedings of FATES 2002, Formal Approaches to Testing of Software. Technical Report, INRIA, August 2002, pp. 105\u2013120 (2002)"},{"key":"2_CR4","unstructured":"AT&T\u00a0Labs-Research. Graphviz - open source graph drawing software. Obtainable at, http:\/\/www.research.att.com\/sw\/tools\/graphviz\/"},{"key":"2_CR5","unstructured":"B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual(1999), Available at, http:\/\/www.b-core.com\/ONLINEDOC\/Contents.html"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems compositionally and automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-46002-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Bouquet","year":"2002","unstructured":"Bouquet, F., Legeard, B., Peureux, F.: CLPS-B - a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 188\u2013204. Springer, Heidelberg (2002)"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Casner, S., Larkin, J.: Cognitive Efficiency Considerations for Good Graphic Design. In: 11th Annual Conf. of the Cognitive Science Society, Ann Arbor, Michigan (August 1989)","DOI":"10.21236\/ADA218976"},{"key":"2_CR9","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"2_CR10","unstructured":"Ham, H.W.F., Wijk, J.: Visualization of State Transition Graphs. In: IEEE Symposium on Information Visualization, San Diego, CA, USA, October 2001, pp. 59\u201363 (2001)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Fitter, M., Green, T.: When Do Diagrams Make Good Programming Languages? Int. Journal of Man-Machine Studies, 235\u2013261 (1979)","DOI":"10.1016\/S0020-7373(79)80019-X"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/3-540-36577-X_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Groote","year":"2003","unstructured":"Groote, J., Ham, F.: Large State Space Visualization. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 585\u2013590. Springer, Heidelberg (2003)"},{"issue":"1","key":"2_CR13","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/2945.841119","volume":"6","author":"I. Herman","year":"2000","unstructured":"Herman, I., Melanon, G., Marshall, M.S.: Graph Visualization and Navigation in Information Visualization: A Survey. IEEE Transactions on Visualization and Computer Graphics\u00a06(1), 24\u201343 (2000)","journal-title":"IEEE Transactions on Visualization and Computer Graphics"},{"key":"2_CR14","volume-title":"Introduction to Automata Theory, Languages and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading (1979)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45687-2_27","volume-title":"Mathematical Foundations of Computer Science 2002","author":"L. Ilie","year":"2002","unstructured":"Ilie, L., Yu, S.: Algorithms for Computing Small NFAs. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol.\u00a02420, p. 328. Springer, Heidelberg (2002)"},{"issue":"6","key":"2_CR16","doi-asserted-by":"publisher","first-page":"1117","DOI":"10.1137\/0222067","volume":"22","author":"T. Jiang","year":"1993","unstructured":"Jiang, T., Ravikunar, B.: Minimal NFA Problems are Hard. SIAM Journal on Computing\u00a022(6), 1117\u20131141 (1993)","journal-title":"SIAM Journal on Computing"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-30500-2_18","volume-title":"Implementation and Application of Automata","author":"S.A. John","year":"2005","unstructured":"John, S.A.: Minimal Unambigous \u03b5-NFA. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol.\u00a03317, pp. 190\u2013201. Springer, Heidelberg (2005)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Turner, E.: Visualising larger states spaces in ProB. Technical report, School of Electronics and Computer Science, University of Southampton (January 2005)","DOI":"10.1007\/11415787_2"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/3-540-45007-6_31","volume-title":"Developments in Language Theory","author":"A. Malcher","year":"2003","unstructured":"Malcher, A.: Minimizing Finite Automata is Computationally Hard. In: \u00c9sik, Z., F\u00fcl\u00f6p, Z. (eds.) DLT 2003. LNCS, vol.\u00a02710, pp. 386\u2013397. Springer, Heidelberg (2003)"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Dulac, N.L.N., Viguier, T., Storey, M.-A.: On the use of Visualization in Formal Requirements Specification. In: IEEE Joint International Conference on Requirements Engineering, Essen, Germany, September 2002, pp. 71\u201381 (2002)","DOI":"10.1109\/ICRE.2002.1048507"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-49059-0_13","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"V. Rusu","year":"1999","unstructured":"Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 178. Springer, Heidelberg (1999)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","first-page":"319","volume-title":"Computer Aided Verification","author":"H. Sadi","year":"1999","unstructured":"Sadi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 319\u2013331. Springer, Heidelberg (1999)"},{"key":"2_CR24","unstructured":"Steria, Aix-en-Provence, France. Atelier B, User and Reference Manuals (1996) Available at, http:\/\/www.atelierb.societe.com\/index_uk.html"}],"container-title":["Lecture Notes in Computer Science","ZB 2005: Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11415787_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:51:49Z","timestamp":1605642709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11415787_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255598","9783540320074"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11415787_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}