{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:00:33Z","timestamp":1725890433709},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851134"},{"type":"electronic","value":"9783540851141"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85114-1_16","type":"book-chapter","created":{"date-parts":[[2008,8,13]],"date-time":"2008-08-13T03:22:48Z","timestamp":1218597768000},"page":"214-231","source":"Crossref","is-referenced-by-count":2,"title":["Resource-Aware Verification Using Randomized Exploration of Large State Spaces"],"prefix":"10.1007","author":[{"given":"Nazha","family":"Abed","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marc","family":"Vincent","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst.\u00a08, 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR3","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":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-60385-9_13","volume-title":"Correct Hardware Design and Verification Methods","author":"U. Stern","year":"1995","unstructured":"Stern, U., Dill, D.L.: Improved probabilistic verification by hash compaction. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 206\u2013224. Springer, Heidelberg (1995)"},{"key":"16_CR5","series-title":"IFIP Conference Proceedings","first-page":"301","volume-title":"PSTV","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J.: An analysis of bistate hashing. In: PSTV. IFIP Conference Proceedings, vol.\u00a038, pp. 301\u2013314. Chapman & Hall, Boca Raton (1995)"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1023\/A:1014728912264","volume":"20","author":"R. Nalumasu","year":"2002","unstructured":"Nalumasu, R., Gopalakrishnan, G.: An efficient partial order reduction algorithm with an alternative proviso implementation. Formal Methods in System Design\u00a020, 231\u2013247 (2002)","journal-title":"Formal Methods in System Design"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"Clarke, E.M., Jha, S., Enders, R., Filkorn, T.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design\u00a09, 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"key":"16_CR8","first-page":"428","volume-title":"LICS","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: LICS, pp. 428\u2013439. IEEE Computer Society, Los Alamitos (1990)"},{"key":"16_CR9","first-page":"21","volume-title":"Probabilistic Algorithms","author":"M.O. Rabin","year":"1976","unstructured":"Rabin, M.O.: Probabilistic Algorithms, pp. 21\u201339. Academic Press, Inc., Orlando (1976)"},{"key":"16_CR10","first-page":"233","volume-title":"Protocol Specification, Testing and Verification","author":"C.H. West","year":"1986","unstructured":"West, C.H.: Protocol validation by random state exploration. In: Protocol Specification, Testing and Verification, pp. 233\u2013242. North-Holland, Amsterdam (1986)"},{"key":"16_CR11","unstructured":"Owen, D., Menzies, T.: Lurch: a lightweight alternative to model checking. In: SEKE, pp. 158\u2013165 (2003)"},{"key":"16_CR12","unstructured":"Haslum, P.: Model checking by random walk. In: ECSEL Workshop (1999)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","first-page":"111","volume-title":"Monterey Workshop","author":"R. Grosu","year":"2006","unstructured":"Grosu, R., Huang, X., Smolka, S.A., Tan, W., Tripakis, S.: Deep random search for efficient model checking of timed automata. In: Monterey Workshop. LNCS, vol.\u00a04888, pp. 111\u2013124. Springer, Heidelberg (2006)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Sivaraj, H., Gopalakrishnan, G.: Random walk based heuristic algorithms for distributed memory model checking. Electr. Notes Theor. Comput. Sci.\u00a089 (2003)","DOI":"10.1016\/S1571-0661(05)80096-9"},{"key":"16_CR16","first-page":"574","volume-title":"ICCAD","author":"A. Kuehlmann","year":"1999","unstructured":"Kuehlmann, A., McMillan, K.L., Brayton, R.K.: Probabilistic state space search. In: ICCAD, pp. 574\u2013579. IEEE, Los Alamitos (1999)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-540-24732-6_3","volume-title":"Model Checking Software","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 23\u201338. Springer, Heidelberg (2004)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-56496-9_15","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State-space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 178\u2013191. Springer, Heidelberg (1993)"},{"key":"16_CR19","first-page":"317","volume-title":"APSEC","author":"E. Tronci","year":"2001","unstructured":"Tronci, E., Penna, G.D., Intrigila, B., Zilli, M.V.: A probabilistic approach to automatic verification of concurrent systems. In: APSEC, pp. 317\u2013324. IEEE Computer Society, Los Alamitos (2001)"},{"key":"16_CR20","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/55483.55496","volume":"17","author":"F.J. Lin","year":"1987","unstructured":"Lin, F.J., Chu, P.M., Liu, M.T.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. SIGCOMM Comput. Commun. Rev.\u00a017, 126\u2013135 (1987)","journal-title":"SIGCOMM Comput. Commun. Rev."},{"key":"16_CR21","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., 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":"16_CR22","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/566171.566175","volume":"27","author":"A. Groce","year":"2002","unstructured":"Groce, A., Visser, W.: Model checking java programs using structural heuristics. SIGSOFT Softw. Eng. Notes\u00a027, 12\u201321 (2002)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"16_CR23","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10009-004-0141-1","volume":"6","author":"P. Godefroid","year":"2004","unstructured":"Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. Int. J. Softw. Tools Technol. Transf.\u00a06, 117\u2013127 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"16_CR24","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/1287624.1287670","volume-title":"ESEC-FSE 2007","author":"S. Sankaranarayanan","year":"2007","unstructured":"Sankaranarayanan, S., Chang, R., Jiang, G., Ivancic, F.: State space exploration using feedback constraint generation and Monte-Carlo sampling. In: ESEC-FSE 2007, pp. 321\u2013330. ACM, New York (2007)"},{"key":"16_CR25","first-page":"101","volume-title":"FMCAD 2007","author":"H. Chockler","year":"2007","unstructured":"Chockler, H., Farchi, E., Godlin, B., Novikov, S.: Cross-entropy based testing. In: FMCAD 2007, pp. 101\u2013108. IEEE, Los Alamitos (2007)"},{"key":"16_CR26","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1002\/rsa.3240060106","volume":"6","author":"U. Feige","year":"1995","unstructured":"Feige, U.: A tight upper bound on the cover time for random walks on graphs. Random Struct. Algorithms\u00a06, 51\u201354 (1995)","journal-title":"Random Struct. Algorithms"},{"key":"16_CR27","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/1081180.1081193","volume-title":"FMICS 2005","author":"R. Pel\u00e1nek","year":"2005","unstructured":"Pel\u00e1nek, R., Han\u017el, T., \u010cern\u00e1, I., Brim, L.: Enhancing random walk state space exploration. In: FMICS 2005, pp. 98\u2013105. ACM, New York (2005)"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/10722167_41","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2000","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: If: A validation environment for timed asynchronous systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 543\u2013547. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85114-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:22:08Z","timestamp":1606184528000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85114-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851134","9783540851141"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85114-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}