{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:24:05Z","timestamp":1725549845615},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540272311"},{"type":"electronic","value":"9783540316862"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_15","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T08:33:28Z","timestamp":1268382808000},"page":"148-152","source":"Crossref","is-referenced-by-count":28,"title":["Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework"],"prefix":"10.1007","author":[{"given":"Matthew B.","family":"Dwyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Hatcliff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Hoosier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Robby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/s100090200074","volume":"4","author":"D. Bosnacki","year":"2002","unstructured":"Bosnacki, D., Dams, D., Holenderski, L.: Symmetric SPIN. International Journal on Software Tools for Technology Transfer\u00a04(1), 92\u2013106 (2002)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"15_CR2","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder \u2013 a second generation of a Java model-checker. In: Proceedings of the Workshop on Advances in Verification (July 2000)"},{"issue":"2","key":"15_CR3","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1109\/32.908961","volume":"27","author":"W. Chan","year":"2001","unstructured":"Chan, W., Anderson, R.J., Beame, P., Notkin, D., Jones, D.H., Warner, W.E.: Optimizing symbolic model checking for statecharts. IEEE Transactions on Software Engineering\u00a027(2), 170\u2013190 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR4","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Deng, W., Dwyer, M., Hatcliff, J., Jung, G.: Model-checking middleware-based event-driven real-time embedded software. In: Proceedings of the 1st Internatiuonal Symposium on Formal Methods for Component and Objects, pp. 154\u2013181 (2002)","DOI":"10.1007\/978-3-540-39656-7_6"},{"issue":"2-3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"M.B. Dwyer","year":"2004","unstructured":"Dwyer, M.B., Hatcliff, J., Robby, Prasad, V.R.: Exploiting object escape and locking information in partial order reduction for concurrent object-oriented programs. Formal Methods in System Design\u00a025(2-3), 199\u2013240 (2004)","journal-title":"Formal Methods in System Design"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B.: Space reductions for model checking quasi-cyclic systems. In: Proceedings of the Third International Conference on Embedded Software, pp. 173\u2013189 (2003)","DOI":"10.1007\/978-3-540-45212-6_12"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B.: Analyzing interaction orderings with model checking. In: Proceedings of the 19th IEEE Conference on Automated Software Engineering, pp. 154\u2013163 (2004)","DOI":"10.1109\/ASE.2004.1342733"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Hatcliff, J., Deng, W., Dwyer, M., Jung, G., Prasad, V.: Cadena: An integrated development, analysis, and verification environment for component-based systems. In: Proceedings of the 25th International Conference on Software Engineering, pp. 160\u2013173 (2003)","DOI":"10.1109\/ICSE.2003.1201197"},{"issue":"5","key":"15_CR10","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 Transactions on Software Engineering\u00a023(5), 279\u2013294 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-24622-0_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Hatcliff","year":"2004","unstructured":"Hatcliff, J., Robby, Dwyer, M.B.: Verifying atomicity specifications for concurrent object-oriented software using model-checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 175\u2013190. Springer, Heidelberg (2004)"},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry reduction criteria for software model checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"key":"15_CR13","unstructured":"SAnToS Laboratory. Bogor website (2003), http:\/\/bogor.projects.cis.ksu.edu"},{"key":"15_CR14","unstructured":"SAnToS Laboratory. Software Model Checking course materials website (2004), http:\/\/model-checking.courses.projects.cis.ksu.edu"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Robby, M.B.: Bogor: An extensible and highly-modular model checking framework. In: Proceedings of the 9th European Software Engineering Conference held jointly with the 11th ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 267\u2013276 (2003)","DOI":"10.1145\/940071.940107"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Robby, M.B., Dwyer, J.: Space-reduction strategies for model checking dynamic software. In: Proceedings of the 2nd Workshop on Software Model Chekcing. Electronic Notes in Theoritical Computer Science, vol.\u00a089(3) (2003)","DOI":"10.1016\/S1571-0661(05)80009-X"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-540-24730-2_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Robby","year":"2004","unstructured":"Robby, E., Rodr\u00edguez, M.B.: Checking strong specifications using an extensible software model checking framework. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 404\u2013420. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:04:59Z","timestamp":1605625499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11513988_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}