{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:59:08Z","timestamp":1725551948064},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540311393"},{"type":"electronic","value":"9783540316220"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_13","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T02:28:57Z","timestamp":1134354537000},"page":"190-206","source":"Crossref","is-referenced-by-count":4,"title":["Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Katia","family":"Hristova","sequence":"first","affiliation":[]},{"given":"Yanhong A.","family":"Liu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","volume-title":"Foundations of Databases","author":"S. Abiteboul","year":"1995","unstructured":"Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley, Reading (1995)"},{"key":"13_CR2","volume-title":"Compilers: Principles, Techniques and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1986)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/3-540-44585-4_18","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., Yannakakis, M.: Analysis of recursive state machines. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 207\u2013220. Springer, Heidelberg (2001)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-46002-0_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Basu","year":"2002","unstructured":"Basu, S., Kumar, K.N., Pokorny, L.R., Ramakrishnan, C.R.: Resource-constrained model checking of recursive programs. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 236\u2013250. Springer, Heidelberg (2002)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/3-540-48224-5_54","volume-title":"Automata, Languages and Programming","author":"M. Benedikt","year":"2001","unstructured":"Benedikt, M., Godefroid, P., Reps, T.W.: Model checking of unrestricted hierarchical state machines. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 652\u2013666. Springer, Heidelberg (2001)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory, pp. 135\u2013150 (1997)","DOI":"10.1007\/3-540-63141-0_10"},{"key":"13_CR8","volume-title":"Verification on infinite structures","author":"O. Burkart","year":"2000","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. North-Holland, Amsterdam (2000)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O. Burkart","year":"1997","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 419\u2013429. Springer, Heidelberg (1997)"},{"issue":"3","key":"13_CR10","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/0167-6423(88)90033-0","volume":"11","author":"J. Cai","year":"1989","unstructured":"Cai, J., Paige, R.: Program derivation by fixed point computation. Science of Computer Programming\u00a011(3), 197\u2013261 (1989)","journal-title":"Science of Computer Programming"},{"key":"13_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-83952-8","volume-title":"Logic programming and databases","author":"S. Ceri","year":"1990","unstructured":"Ceri, S., Gottlob, G., Tanca, L.: Logic programming and databases. Springer, New York (1990)"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logic of Programs, Workshop","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, London, UK, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/567067.567080","volume-title":"POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages","author":"E.M. Clarke","year":"1983","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: POPL 1983: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 117\u2013126. ACM Press, New York (1983)"},{"key":"13_CR14","volume-title":"Model Checking","author":"J. Edmund","year":"1999","unstructured":"Edmund, J., Clark, M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"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: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"13_CR17","series-title":"Electronic Notes in Theoretic Comp. Sci","volume-title":"Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997)","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. In: Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997). Electronic Notes in Theoretic Comp. Sci, vol.\u00a09. Elsevier, Amsterdam (1997)"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1145\/888251.888268","volume-title":"Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming","author":"Y.A. Liu","year":"2003","unstructured":"Liu, Y.A., Stoller, S.D.: From datalog rules to efficient programs with time and space guarantees. In: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, pp. 172\u2013183. ACM Press, New York (2003)"},{"key":"13_CR19","unstructured":"Paige, R.: Real-time simulation of a set machine on a ram (1989)"},{"issue":"3","key":"13_CR20","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1145\/357172.357177","volume":"4","author":"R. Paige","year":"1982","unstructured":"Paige, R., Koenig, S.: Finite differencing of computable expressions. ACM Trans. Program. Lang. Syst.\u00a04(3), 402\u2013454 (1982)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR21","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proceedings of the 5th Colloquium on 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: Proceedings of the 5th Colloquium on International Symposium on Programming, London, UK, pp. 337\u2013351. Springer, London (1982)"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, pp. 49\u201361 (1995)","DOI":"10.1145\/199448.199462"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Snodgrass, R.T., Winslett, M. (eds.) Proceedings of the 1994 ACM SIGMOD International Conference on Management of Data SIGMOD 1994, pp. 442\u2013453 (1994)","DOI":"10.1145\/191839.191927"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","first-page":"115","volume-title":"Theoretical Aspects of Computer Software","author":"B. Steffen","year":"1991","unstructured":"Steffen, B.: Generating data flow analysis algorithms from modal specifications. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol.\u00a0526, pp. 115\u2013139. Springer, Heidelberg (1991)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-60218-6_6","volume-title":"CONCUR \u201995 Concurrency Theory","author":"B. Steffen","year":"1995","unstructured":"Steffen, B., Classen, A., Klein, M., Knoop, J., Margaria, T.: The fixpoint-analysis machine. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 72\u201387. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:06:58Z","timestamp":1619492818000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11609773_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}