{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,30]],"date-time":"2025-06-30T10:34:39Z","timestamp":1751279679650},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421245"},{"type":"electronic","value":"9783540451396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_6","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"80-102","source":"Crossref","is-referenced-by-count":39,"title":["Addressing dynamic issues of program model checking"],"prefix":"10.1007","author":[{"given":"Flavio","family":"Lerda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"J. Barnat, L. Brim, and J. Stribrna. Distributed LTL model-checking in SPIN. Technical Report FIMU-RS-2000-10, Faculty of Informatics, Masaryk University, 2000. Available in this LNCS volume.","DOI":"10.1007\/3-540-45139-0_13"},{"key":"6_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 7th International SPIN Workshop","author":"D. Bosnacki","year":"2000","unstructured":"D. Bosnacki, D. Dams, and L. Holenderski. Symmetric SPIN. In Proc. of the 7th International SPIN Workshop, volume 1885 of LNCS. Springer-Verlag, September 2000."},{"issue":"1","key":"6_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/291251.289435","volume":"34","author":"N. Benton","year":"1998","unstructured":"Nick Benton, Andrew Kennedy, and George Russell. Compiling standard ML to Java bytecodes. SIGPLAN Notices, 34(1):129\u2013140, September 1998.","journal-title":"SIGPLAN Notices"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"J. Bormann, J. Lohse, M. Payer, and G. Venzl. Model checking in industrial hardware design. In Proc. of the 32nd Design Automation Conference, 1995.","DOI":"10.1145\/217474.217545"},{"key":"6_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"Proc. of the 7th International SPIN Workshop","author":"T. Ball","year":"2000","unstructured":"Thomas Ball and Sriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Proc. of the 7th International SPIN Workshop, volume 1885 of LNCS, pages 113\u2013130. Springer-Verlag, September 2000."},{"issue":"1","key":"6_CR6","first-page":"20","volume":"6","author":"L.R. Clausen","year":"1998","unstructured":"L.R. Clausen and O. Danvy. Compiling proper tail recursion and first-class continuations: Scheme on the Java Virtual Machine. The Journal of C Language Translation, 6(1):20\u201332, April 1998.","journal-title":"The Journal of C Language Translation"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcli, S. Laubach, C. Pasareanu, and R. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. of the 22nd International Conference on Software Engineering, June 2000.","DOI":"10.1145\/337180.337234"},{"key":"6_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Proc. of the 10th International Conference on Computer Aided Verification","author":"E. M. Clarke","year":"1998","unstructured":"Edmund M. Clarke, E. Allen Emerson, Somesh Jha, and A. Prasad Sistla. Symmetry reductions in model checking. In Proc. of the 10th International Conference on Computer Aided Verification, volume 1427 of LNCS, pages 147\u2013158. Springer-Verlag, 1998."},{"key":"6_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0028174","volume-title":"Proc. of the 5th International Conference on Computer Aided Verification","author":"E. M. Clarke","year":"1993","unstructured":"Edmund M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetries in temporal logic model checking. In Proc. of the 5th International Conference on Computer Aided Verification, volume 697 of LNCS. Springer-Verlag, 1993."},{"key":"6_CR10","unstructured":"Edmund M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. Technical Report CMU-CS-96-178, Carnegie Mellon University, 1996."},{"issue":"7","key":"6_CR11","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V","volume":"29","author":"C. Demartini","year":"1999","unstructured":"Claudio Demartini, Radu Iosif, and Riccardo Sisto. A deadlock detection tool for concurrent Java programs. Software-Practice and Experience, 29(7):577\u2013603, 1999.","journal-title":"Software-Practice and Experience"},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 5th International Conference on Computer Aided Verification","author":"E. Emerson","year":"1993","unstructured":"E. Emerson and C. Jutla. Symmetry and model checking. In Proc. 5th International Conference on Computer Aided Verification, volume 697 of LNCS. Springer-Verlag, 1993."},{"key":"6_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1007\/3-540-63166-6_52","volume-title":"Proc of the 9th International Conference on Computer Aided Verification","author":"P. Godefroid","year":"1997","unstructured":"Patrice Godefroid. VeriSoft: A tool for the automatic analysis of concurrent reactive software. In Proc of the 9th International Conference on Computer Aided Verification, volume 1254 of LNCS, pages 476\u2013479. Springer-Verlag, June 1997."},{"key":"6_CR14","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991."},{"issue":"5","key":"6_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"Gerard J. Holzmann. The SPIN model checker. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR16","unstructured":"Gerard J. Holzmann. State compression in SPIN: Recursive indexing and compression training runs. In Proc. of the 3th International SPIN Workshop, April 1997."},{"key":"6_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 7th International SPIN Workshop","author":"G. J. Holzmann","year":"2000","unstructured":"Gerard J. Holzmann. Logic verification of ANSI-C code with SPIN. In Proc. of the 7th International SPIN Workshop, volume 1885 of LNCS. Springer-Verlag, September 2000."},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"[HP98]Klaus Havelund and Thomas Pressburger. Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer, 2(4), April 1998.","DOI":"10.1007\/s100090050043"},{"issue":"1\/2","key":"6_CR19","first-page":"47","volume":"9","author":"C. N. Ip","year":"1996","unstructured":"C. Norris Ip and David L. Dill. Better verification through symmetry. Formal Methods in System Design, 9(1\/2):47\u201375, August 1996.","journal-title":"Formal Methods in System Design"},{"key":"6_CR20","series-title":"Lect Notes Comput Sci","first-page":"261","volume-title":"Proc. of the 6th International SPIN Workshop","author":"R. Iosif","year":"1999","unstructured":"Radu Iosif and Riccardo Sisto. dSPIN: A dynamic extension of SPIN. In Proc. of the 6th International SPIN Workshop, volume 1680 of LNCS, pages 261\u2013276. Springer-Verlag, September 1999."},{"key":"6_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/10722468_2","volume-title":"Proc. of the 7th International SPIN Workshop","author":"R. Iosif","year":"2000","unstructured":"Radu Iosif and Riccardo Sisto. Using garbage collection in model checking. In Proc. of the 7th International SPIN Workshop, volume 1885 of LNCS, pages 20\u201333. Springer-Verlag, September 2000."},{"key":"6_CR22","unstructured":"Flavio Lerda. Model checking: Tecniche di verifica formale in ambiente distributo. Master\u2019s thesis, Politecnico di Torino, May 2000."},{"key":"6_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proc. of the 5th International SPIN Workshop","author":"F. Lerda","year":"1999","unstructured":"Flavio Lerda and Riccardo Sisto. Distributed-memory model checking with SPIN. In Proc. of the 5th International SPIN Workshop, volume 1680 of LNCS. Springer-Verlag, 1999."},{"key":"6_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Proc. of the 9th International Conference on Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Ulrich Stern and David L. Dill. Parallelizing the Murphi verifier. In Proc. of the 9th International Conference on Computer Aided Verification, volume 1254 of LNCS, pages 256\u2013278. Springer-Verlag, June 1997."},{"key":"6_CR25","unstructured":"SpaceViews. Premature engine cuto likely cause of Mars Polar Lander failure. http:\/\/www.spaceviews.com\/2000\/03\/28b.html , March 2000."},{"key":"6_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/10722468_14","volume-title":"Proc. of the 7th International SPIN Workshop","author":"S. D. Stoller","year":"2000","unstructured":"Scott D. Stoller. Model-checking multi-threaded distributed Java programs. In Proc. of the 7th International SPIN Workshop, volume 1885 of LNCS, pages 224\u2013244. Springer-Verlag, September 2000."},{"key":"6_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0013475","volume-title":"In Ada-Europe International Conference on Reliable Software Technologies","author":"S.T. Taft","year":"1996","unstructured":"S. Tucker Taft. Programming the Internet in Ada 95. In Ada-Europe International Conference on Reliable Software Technologies, volume 1088 of LNCS, pages 1\u201316. Springer-Verlag, June 1996."},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Willem Visser, Klaus Havelund, Guillaume Brat, and Seung-Joon Park. Model checking programs. In Proc. of the 15th IEEE International Conference on Automated Software Engineering, September 2000.","DOI":"10.1109\/ASE.2000.873645"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:17:34Z","timestamp":1556749054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}