{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T04:59:29Z","timestamp":1773723569470,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540213147","type":"print"},{"value":"9783540247326","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24732-6_6","type":"book-chapter","created":{"date-parts":[[2010,7,27]],"date-time":"2010-07-27T20:14:47Z","timestamp":1280261687000},"page":"76-91","source":"Crossref","is-referenced-by-count":58,"title":["Model-Driven Software Verification"],"prefix":"10.1007","author":[{"given":"Gerard J.","family":"Holzmann","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Joshi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Bosnacki, D.: Enhancing state space reduction techniques for model checking. Ph.D Thesis, Eindhoven Univ. of Technology, The Netherlands (2001)"},{"key":"6_CR2","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":"6_CR3","first-page":"439","volume-title":"Proc. 22nd Int. Conf. on Softw. Eng.","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.C., et al.: Bandera: Extracting finite state models from Java source code. In: Proc. 22nd Int. Conf. on Softw. Eng., Limerick, Ireland, June 2000, pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On Model-Checking for Fragments of mu-Calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 385\u2013396. Springer, Heidelberg (1993)"},{"key":"6_CR5","volume-title":"Proc. 2002 Aerospace Conference","author":"P.R. Gluck","year":"2002","unstructured":"Gluck, P.R., Holzmann, G.J.: Using Spin Model Checking for Flight Software Verification. In: Proc. 2002 Aerospace Conference, March 2002, IEEE, Big Sky (2002)"},{"key":"6_CR6","first-page":"431","volume-title":"Proc. 22nd Int. Conf. on Softw. Eng.","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Chandra, S., Palm, C.: Software model checking in practice: an industrial case study. In: Proc. 22nd Int. Conf. on Softw. Eng., Orlando, Fl, May 2002, pp. 431\u2013441. ACM Press, New York (2002)"},{"issue":"4","key":"6_CR7","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java Pathfinder. Int. Journal on Software Tools for Technology Transfer\u00a02(4), 366\u2013381 (2000)","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_8","volume-title":"SPIN Model Checking and Software Verification","author":"G.J. Holzmann","year":"2000","unstructured":"Holzmann, G.J.: Logic Verification of ANSI-C Code with Spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, Springer, Heidelberg (2000)"},{"key":"6_CR9","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"issue":"4","key":"6_CR10","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1109\/TSE.2002.995426","volume":"28","author":"G.J. Holzmann","year":"2002","unstructured":"Holzmann, G.J., Smith, M.H.: An automated verification method for distributed systems software based on model extraction. IEEE Trans. on Software Engineering\u00a028(4), 364\u2013377 (2002)","journal-title":"IEEE Trans. on Software Engineering"},{"key":"6_CR11","volume-title":"Specifying Systems: the TLA+ language and tools for hardware and software engineers","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley, Reading (2002)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Proc. Fifth Symposium on Operating Systems Design and Implementation (December 2002)","DOI":"10.1145\/1060289.1060297"},{"key":"6_CR13","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"5th GI-Conference on Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"6_CR14","unstructured":"http:\/\/f2.org\/maths\/ttt.html"},{"key":"6_CR15","unstructured":"http:\/\/cm.bell-labs.com\/cm\/cs\/what\/modex\/"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24732-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,17]],"date-time":"2019-01-17T18:02:29Z","timestamp":1547748149000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24732-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540213147","9783540247326"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24732-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}