{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:37:39Z","timestamp":1725557859864},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540201755"},{"type":"electronic","value":"9783540399797"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39979-7_6","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T18:52:22Z","timestamp":1277232742000},"page":"79-94","source":"Crossref","is-referenced-by-count":5,"title":["Generation of All Counter-Examples for Push-Down Systems"],"prefix":"10.1007","author":[{"given":"Samik","family":"Basu","sequence":"first","affiliation":[]},{"given":"Diptikalyan","family":"Saha","sequence":"additional","affiliation":[]},{"given":"Yow-Jian","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Scott A.","family":"Smolka","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Alur, R., Dang, T., Ivan\u010di\u0107, F.: Counter-example guided predicate abstraction of hybrid systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: Symposium on Principles of Programming Languages (2003)","DOI":"10.1145\/604131.604140"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Basu, S., Kumar, K.N., Pokorny, R.L., Ramakrishnan, C.R.: Resource-constrained model checking for recursive programs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2002)","DOI":"10.1007\/3-540-46002-0_17"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. Concurrency Theory (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems\u00a08(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: 12th International Conference Computer Aided Verification (2000)","DOI":"10.1007\/10722167_15"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L.: Counter-example based predicate discovery in predicate abstraction. In: 4th International Conference on Formal Methods in Computer-Aided Design (2002)","DOI":"10.1007\/3-540-36126-X_2"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"12th International Conference Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: 12th International Conference Computer Aided Verification, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"13th International Conference Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: 13th International Conference Computer Aided Verification, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"6_CR10","volume-title":"2nd International Workshop on Verification of Infinite State System","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: 2nd International Workshop on Verification of Infinite State System, vol.\u00a09. Elsevier Science, Amsterdam (1997)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Glusman, M., Kamhi, G., Mador-Haim, S., Fraer, R., Vardi, M.Y.: Multiple-counterexample guided iterative abstraction refinement: An industrial evaluation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2003)","DOI":"10.1007\/3-540-36577-X_13"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2002)","DOI":"10.1007\/3-540-46002-0_25"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: SPINWorkshop (2003)","DOI":"10.1007\/3-540-44829-2_8"},{"key":"6_CR14","volume-title":"Elements of the Theory of Computation","author":"H.R. Lewis","year":"1998","unstructured":"Lewis, H.R., Papadimitriou, C.H.: Elements of the Theory of Computation. Prentice Hall Inc., Englewood Cliffs (1998)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.: Certifying model checkers. In: 13th International Conference Computer Aided Verification (2001)","DOI":"10.1007\/3-540-44585-4_2"},{"key":"6_CR16","unstructured":"Pace, G., Halbwachs, N., Raymond, P.: Counter-example generation in symbolic abstract model-checking. In: 6th International Workshop on Formal Methods for Industrial Critical Systems, Paris, Inria (2001)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible counter-examples when model checking abstracted Java programs. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2001)","DOI":"10.1007\/3-540-45319-9_20"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (1982)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Sai\u030bdi, H.: Model checking guided abstraction and analysis. In: Static Analysis Symposium (2000)","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-58950-3_371","volume-title":"Graph Drawing","author":"G. Sander","year":"1995","unstructured":"Sander, G.: Graph layout through the VCG tool. In: Tamassia, R., Tollis, I.G. (eds.) GD 1994. LNCS, vol.\u00a0894, pp. 194\u2013205. Springer, Heidelberg (1995)"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Sekar, R., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A.: Model-carrying code: A new paradigm for mobile-code security. In: New Security Paradigms Workshop, Cloudcroft, New Mexico (2001)","DOI":"10.1145\/508171.508175"},{"key":"6_CR22","unstructured":"XSB. The XSB logic programming system, Available from http:\/\/xsb.sourceforge.net"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Networked and Distributed Systems - FORTE 2003"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39979-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T09:36:34Z","timestamp":1559208994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39979-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540201755","9783540399797"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39979-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}