{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:34:15Z","timestamp":1725496455971},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668565"},{"type":"electronic","value":"9783540466741"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46674-6_18","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T15:50:17Z","timestamp":1196351417000},"page":"201-213","source":"Crossref","is-referenced-by-count":1,"title":["Demand-Driven Model Checking for Context-Free Processes"],"prefix":"10.1007","author":[{"given":"Jens","family":"Knoop","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,19]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/BF01386340","volume":"4","author":"J. W. Backus","year":"1963","unstructured":"J. W. Backus, F. L. Bauer, J. Green, and et al. Revised report on the algorithmic language ALGOL60. Numer. Math., 4:420\u2013453, 1963.","journal-title":"Numer. Math."},{"key":"18_CR2","first-page":"135","volume":"1243","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proc. 8th Int. Conf. on Concurrency Theory (CONCUR\u201997), LNCS 1243, pages 135\u2013150. Springer-V., 1997.","journal-title":"Proc. 8th Int. Conf. on Concurrency Theory (CONCUR\u201997)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"J. C. Bradfield. Verifying Temporal Properties of Systems. Birkh\u00e4user, Boston,1992.","DOI":"10.1007\/978-1-4684-6819-9"},{"key":"18_CR4","first-page":"115","volume":"458","author":"J. C. Bradfield","year":"1990","unstructured":"J. C. Bradfield and C. P. Stirling. Verifying temporal properties of processes. In Proc. 1st Int. Conf. on Concurrency Theory (CONCUR\u201990), LNCS 458, pages115\u2013125. Springer-V., 1990.","journal-title":"Proc. 1st Int. Conf. on Concurrency Theory (CONCUR\u201990)"},{"key":"18_CR5","first-page":"123","volume":"630","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In Proc.3rd Int. Conf. on Concurrency Theory (CONCUR\u201992), LNCS 630, pages 123\u2013137. Springer-V., 1992.","journal-title":"Proc.3rd Int. Conf. on Concurrency Theory"},{"key":"18_CR6","first-page":"98","volume":"836","author":"O. Burkart","year":"1994","unstructured":"O. Burkart and B. Steffen. Pushdown processes: Parallel composition and model checking. In Proc. 5th Int. Conf. on Concurrency Theory (CONCUR\u201994), LNCS836, pages 98\u2013113. Springer-V., 1994.","journal-title":"Proc. 5th Int. Conf. on Concurrency Theory (CONCUR\u201994)"},{"key":"18_CR7","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume":"131","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proc. IBM Workshop on Logic of Programs (LoP\u201981), LNCS 131, pages 52\u201371. Springer-V., 1981.","journal-title":"Proc. IBM Workshop on Logic of Programs (LoP\u201981)"},{"issue":"1","key":"18_CR8","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Workbench: A semantics based verification tool for finite state systems. ACM Trans. Prog. Lang. Syst., 15(1):36\u201372, 1993.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"6","key":"18_CR9","doi-asserted-by":"publisher","first-page":"992","DOI":"10.1145\/267959.269970","volume":"19","author":"E. Duesterwald","year":"1997","unstructured":"E. Duesterwald, R. Gupta, and M. L. Soffa. A practical framework for demand driven interprocedural data flow analysis. ACM Trans. Prog. Lang. Syst.,19(6):992\u20131030, 1997.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"18_CR10","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. 1st IEEE Annual Symp. on Logic in Computer Science (LICS\u201986), pages 267\u2013278. IEEE Computer Society, 1986."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"S. Horwitz, T. Reps, and M. Sagiv. Demand interprocedural dataflow analysis. In Proc. 3rd ACM SIGSOFT Symp. on the Foundations of Software Engineering (FSE\u201995), pages 104\u2013115, 1995.","DOI":"10.1145\/222124.222146"},{"key":"18_CR12","first-page":"593","volume":"700","author":"H. Hungar","year":"1993","unstructured":"H. Hungar and B. Steffen. Local model checking for context-free processes. In Proc. 20th Colloquium on Automata, Languages, and Programming (ICALP\u201993), LNCS 700, pages 593\u2013605. Springer-V., 1993.","journal-title":"Proc. 20th Colloquium on Automata, Languages, and Programming (ICALP\u201993)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"J. Knoop. Optimal Interprocedural Program Optimization: A new Framework and its Application. PhD thesis, Univ. of Kiel, Germany, 1993. LNCS Tutorial 1428, Springer-V., 1998.","DOI":"10.1007\/3-540-49639-4"},{"key":"18_CR14","first-page":"12","volume":"18","author":"R. Mayr","year":"1998","unstructured":"R. Mayr. Strict lower bounds for model checking BPA. ENTCS, 18:12 pages,1998.","journal-title":"ENTCS"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"18_CR16","first-page":"337","volume":"137","author":"J. P. Queille","year":"1982","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Symp. on Programming (SoP\u201982), LNCS 137, pages337\u2013351. Springer-V., 1982.","journal-title":"Proc. 5th Int. Symp. on Programming (SoP\u201982)"},{"key":"18_CR17","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-57877-3_26","volume":"786","author":"T. Reps","year":"1994","unstructured":"T. Reps. Solving demand versions of interprocedural analysis problems. In Proc.5th Int. Conf. on Compiler Construction (CC\u201994), LNCS 786, pages 389\u2013403.Springer-V., 1994.","journal-title":"Proc.5th Int. Conf. on Compiler Construction (CC\u201994)"},{"key":"18_CR18","unstructured":"M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189\u2013233. Prentice Hall, Englewood Cli_s, NJ,1981."},{"key":"18_CR19","first-page":"72","volume":"962","author":"B. Steffen","year":"1995","unstructured":"B. Steffen, A. Claren, M. Klein, J. Knoop, and T. Margaria. The fixpoint-analysis machine. In Proc. 6th Int. Conf. on Concurrency Theory (CONCUR\u201995), LNCS962, pages 72\u201387. Springer-V., 1995. Invited contribution.","journal-title":"Proc. 6th Int. Conf. on Concurrency Theory (CONCUR\u201995)"},{"key":"18_CR20","first-page":"369","volume":"351","author":"C. Stirling","year":"1989","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In Proc. 3rd Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT\u201989), LNCS 351, pages 369\u2013383. Springer-V., 1989.","journal-title":"Proc. 3rd Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT\u201989)"},{"issue":"1","key":"18_CR21","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. TCS,89(1):161\u2013177, 1991.","journal-title":"TCS"},{"key":"18_CR22","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume":"1102","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown processes: Games and model checking. In Proc. 8th Int. Workshop on Computer Aided Verification (CAV\u201996), LNCS 1102, pages 62\u201374. Springer-V., 1996.","journal-title":"Proc. 8th Int. Workshop on Computer Aided Verification (CAV\u201996)"}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science \u2014 ASIAN\u201999"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46674-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,5]],"date-time":"2019-05-05T08:56:23Z","timestamp":1557046583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46674-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668565","9783540466741"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-46674-6_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}