{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T05:45:59Z","timestamp":1648619159496},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2004,8,1]],"date-time":"2004-08-01T00:00:00Z","timestamp":1091318400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2004,8]]},"DOI":"10.1007\/s10009-004-0168-3","type":"journal-article","created":{"date-parts":[[2004,11,16]],"date-time":"2004-11-16T12:05:32Z","timestamp":1100606732000},"page":"257-259","source":"Crossref","is-referenced-by-count":1,"title":["Introductory paper"],"prefix":"10.1007","volume":"6","author":[{"given":"Matthew","family":"Dwyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Leue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,11,17]]},"reference":[{"key":"168_CR1","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2001) Automatically validating temporal safety properties of interfaces. In: Proceedings of SPIN 2001. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45139-0_7"},{"key":"168_CR2","doi-asserted-by":"crossref","unstructured":"Bengtsson J, Larsen KG, Larsson F, Pettersson P, Yi W (1997) UPPAAL \u2013 a tool suite for automatic verification of real-time systems. In: Alur R, Henzinger TA, Sonntag ED (eds) Hybrid systems III \u2013 Verification and control. Lecture notes in computer science, vol 1066. Springer, Berlin Heidelberg New York, pp 232\u2013243","DOI":"10.1007\/BFb0020949"},{"key":"168_CR3","doi-asserted-by":"crossref","unstructured":"B\u00e9rard B, Finkel M, Bidoit A, Laroussine F, Petit A, Petrucci L, Schoenebelen P, McKenzie P (2001) Systems and software verification. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-3-662-04558-9"},{"key":"168_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"Clarke","year":"1992","unstructured":"Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"168_CR5","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"168_CR6","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/s100090050030","volume":"2","author":"Cleaveland","year":"1999","unstructured":"Cleaveland R (1999) Pragmatics of model checking: an STTT special section. Int J Softw Tools Technol Transfer 2(3):208\u2013218","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"168_CR7","doi-asserted-by":"crossref","unstructured":"Corbett JC, Dwyer MB, Hatcliff J, Laubach S, Pasareanu CS, Robby, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: 22nd IEEE international conference on software engineering (ICSE)","DOI":"10.1145\/337180.337234"},{"key":"168_CR8","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Leue S, Lluch-Lafuente A (2004) Directed explicit-state model checking in the validation of communication protocols. Int J Softw Tools Technol Transfer 5(2\u20133):247\u2013267. DOI: 10.1007\/s10009-002-0104-3","DOI":"10.1007\/s10009-002-0104-3"},{"key":"168_CR9","first-page":"the","volume":"checking","author":"Godefroid","year":"2003","unstructured":"Godefroid P (2003) Software model checking: the VeriSoft approach. Technical report, Bell Labs Technical Memorandum ITD-03-44189G. Formal Meth Syst Des (in press)","journal-title":"Software model"},{"key":"168_CR10","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"Havelund","year":"2000","unstructured":"Havelund K, Pressburger T (2000) Model checking Java programs using Java PathFinder. Int J Softw Tools Technol Transfer 2(4):366\u2013381","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"168_CR11","doi-asserted-by":"crossref","unstructured":"Havelund K, Visser W (2002) Program model checking as a new trend. Int J Softw Tools Technol Transfer 4(1):8\u201320. DOI: 10.1007\/s10009-002-0080-7","DOI":"10.1007\/s10009-002-0080-7"},{"key":"168_CR12","unstructured":"Holzmann GJ (2003) The SPIN model checker, primer and reference manual. Addison-Wesley, Reading, MA"},{"key":"168_CR13","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"Holzmann","year":"2000","unstructured":"Holzmann GJ, Smith MH (2000) Automating software feature verification. Bell Labs Tech J 5(2):72\u201387","journal-title":"Bell Labs Tech J"},{"key":"168_CR14","unstructured":"Iosif R, Sisto R (1999) dSPIN: A dynamic extension of SPIN. In: Proceedings of the 6th SPIN workshop. Lecture notes in computer science, vol 1680. Springer, Berlin Heidelberg New York, pp 261\u2013276"},{"key":"168_CR15","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking. Kluwer, Dordrecht","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"168_CR16","doi-asserted-by":"crossref","unstructured":"Peled DA (2001) Software reliability methods. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"168_CR17","doi-asserted-by":"crossref","unstructured":"Visser W, Havelund K, Brat G, Park S (2000) Model checking programs. In: IEEE International conference on automated software engineering. September 2000","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0168-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0168-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0168-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T03:33:59Z","timestamp":1585971239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0168-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8]]},"references-count":17,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,8]]}},"alternative-id":["168"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0168-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,8]]}}}