{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T01:30:40Z","timestamp":1785202240796,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198281","type":"print"},{"value":"9783642198298","type":"electronic"}],"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-19829-8_1","type":"book-chapter","created":{"date-parts":[[2011,3,16]],"date-time":"2011-03-16T10:20:41Z","timestamp":1300270841000},"page":"1-16","source":"Crossref","is-referenced-by-count":8,"title":["Directed Model Checking for B: An Evaluation and New Techniques"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jens","family":"Bendisposto","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_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":"1_CR2","volume-title":"Principles of the Spin Model Checker","author":"M. Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the Spin Model Checker. Springer, Heidelberg (2008)"},{"issue":"2","key":"1_CR3","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation\u00a098(2), 142\u2013170 (1992)","journal-title":"Information and Computation"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11691617_2","volume-title":"Model Checking Software","author":"K. Dr\u00e4ger","year":"2006","unstructured":"Dr\u00e4ger, K., Finkbeiner, B., Podelski, A.: Directed model checking with distance-preserving abstractions. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 19\u201334. Springer, Heidelberg (2006)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"1_CR6","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT\u00a05(2-3), 247\u2013267 (2004)","journal-title":"STTT"},{"issue":"4","key":"1_CR7","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10009-004-0151-z","volume":"6","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Partial-order reduction and trail improvement in directed model checking. STTT\u00a06(4), 277\u2013301 (2004)","journal-title":"STTT"},{"issue":"3","key":"1_CR8","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1145\/5666.5673","volume":"29","author":"P.J. Fleming","year":"1986","unstructured":"Fleming, P.J., Wallace, J.J.: How not to lie with statistics: the correct way to summarize benchmark results. ACM Commun.\u00a029(3), 218\u2013221 (1986)","journal-title":"ACM Commun."},{"key":"1_CR9","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement \u2014 FDR2 User Manual (version 2.8.2)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-46017-9_21","volume-title":"Model Checking Software","author":"A. Groce","year":"2002","unstructured":"Groce, A., Visser, W.: Heuristic model checking for Java programs. In: Bosnacki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 242\u2013245. Springer, Heidelberg (2002)"},{"issue":"5","key":"1_CR11","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker Spin. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"issue":"3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1023\/A:1008696026254","volume":"13","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. Formal Methods in System Design\u00a013(3), 289\u2013307 (1998)","journal-title":"Formal Methods in System Design"},{"key":"1_CR13","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"1_CR14","series-title":"IFIP Conference Proceedings","first-page":"197","volume-title":"FORTE","author":"G.J. Holzmann","year":"1994","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Hogrefe, D., Leue, S. (eds.) FORTE. IFIP Conference Proceedings, vol.\u00a06, pp. 197\u2013211. Chapman and Hall, Boca Raton (1994)"},{"key":"1_CR15","series-title":"ACM International Conference Proceeding Series","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/1456659.1456673","volume-title":"SAICSIT Conf.","author":"T. H\u00f6rne","year":"2008","unstructured":"H\u00f6rne, T., van der Poll, J.A.: Planning as model checking: the performance of ProB vs NuSMV. In: Botha, R., Cilliers, C. (eds.) SAICSIT Conf. ACM International Conference Proceeding Series, vol.\u00a0338, pp. 114\u2013123. ACM, New York (2008)"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology\u00a011, 256\u2013290 (2002)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"1_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":"1_CR18","doi-asserted-by":"crossref","unstructured":"Leuschel, M., Bendisposto, J.: Directed model checking for B: An evaluation and new techniques. Technical report, STUPS, Universit\u00e4t D\u00fcsseldorf (September 2010), http:\/\/www.stups.uni-duesseldorf.de\/publications_detail.php?id=312","DOI":"10.1007\/978-3-642-19829-8_1"},{"key":"1_CR19","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)"},{"issue":"2","key":"1_CR20","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":"1_CR21","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. PhD thesis, Boston (1993)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"key":"1_CR23","unstructured":"Samia, M., Wiegard, H., Bendisposto, J., Leuschel, M.: High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin. In: Attiogbe, Mery (eds.) Proceedings TFM-B 2009, pp. 49\u201361. APCB (June 2009)"},{"key":"1_CR24","unstructured":"Wiegard, H.: A comparison of the model checker ProB with Spin. Master thesis, Institut f\u00fcr Informatik, Universit\u00e4t D\u00fcsseldorf, Bachelor\u2019s thesis (2008)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y. Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA $^{\\mbox{+}}$ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 54\u201366. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19829-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,20]],"date-time":"2021-11-20T06:12:23Z","timestamp":1637388743000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19829-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198281","9783642198298"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19829-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}