{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:31:00Z","timestamp":1743082260934,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_26","type":"book-chapter","created":{"date-parts":[[2010,6,26]],"date-time":"2010-06-26T00:08:38Z","timestamp":1277510918000},"page":"462-481","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems"],"prefix":"10.1007","author":[{"given":"Marc","family":"Lettrari","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"issue":"7","key":"26_CR1","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"R.J. Anderson","year":"1998","unstructured":"Anderson, R.J., Beame, P., Burns, S., Chan, W., Modugno, F., Notkin, D., Reese, J.D.: Model Checking Large Software Specifications. IEEE Transactions on Software Engineering\u00a024(7), 498\u2013520 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"2","key":"26_CR3","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"4","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation Framework. Journal of Logic and Computation\u00a04(2), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexampleguided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013196. Springer, Heidelberg (2000)"},{"key":"26_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"26_CR6","unstructured":"Dwyer, M., Hatcliff, J., Joehanes, R., Laubach, S., Pasareanu, C., Visser, W., Zheng, H.: Tool-supported Program Abstraction for Finite-state Verification. In: Proceedings ICSE 2001 (2001)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-Spin. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 57\u201379. Springer, Heidelberg (2001)"},{"key":"26_CR8","unstructured":"Edelkamp, S., Lafuente, A.L., Leue, S.: Protocol verification with heuristic search. In: AAAI Symposium on Model-based Validation of Intelligence (2001)"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. In: Proc. 5th Conference on Computer Aided Verification, pp. 463\u2013478 (1993)","DOI":"10.1007\/3-540-56922-7_38"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46002-0_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Khurshid, S.: Exploring very large state spaces using Genetic Algorithms. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 1\u201310. Springer, Heidelberg (2002)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"26_CR12","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: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, p. 242. Springer, Heidelberg (2002)"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: Model Checking Java Programs using Strucural Heuristics. In: Proceedings of ISSTA 2002, Rome, Italy (2002)","DOI":"10.1145\/566172.566175"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. In: Proceedings of the 6th IEEE Symposium on Logic in Computer Science, Amsterdam, July 1991, pp. 406\u2013415 (1991)","DOI":"10.1109\/LICS.1991.151664"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSSC.1968.300136","volume":"4","author":"P.E. Hart","year":"1968","unstructured":"Hart, P.E., Nilsson, N.J., Raphael, B.: A formal basis for heuristic determination of minimum path cost. IEEE Transactions on Systems Science and Cybernetics\u00a04, 100\u2013107 (1968)","journal-title":"IEEE Transactions on Systems Science and Cybernetics"},{"key":"26_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T08:01:57Z","timestamp":1740211317000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}