{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T13:49:18Z","timestamp":1761918558613},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,10,22]],"date-time":"2002-10-22T00:00:00Z","timestamp":1035244800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1007\/s10009-002-0095-0","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:55:36Z","timestamp":1079798136000},"page":"49-58","source":"Crossref","is-referenced-by-count":47,"title":["Boolean and Cartesian abstraction for model checking C programs"],"prefix":"10.1007","volume":"5","author":[{"given":"Thomas","family":"Ball","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Sriram K.","family":"Rajamani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,22]]},"reference":[{"key":"95_CR1","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K. (2001) Automatic predicate abstraction of C programs. In: PLDI 01: programming language design and implementation. ACM, New York","DOI":"10.1145\/378795.378846"},{"key":"95_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K. (2000) Bebop: a symbolic model checker for Boolean programs. In: SPIN 00: SPIN Workshop, Lecture Notes in Computer Science, vol. 1885. Springer, Berlin Heidelberg New York, pp. 113\u2013130","DOI":"10.1007\/10722468_7"},{"key":"95_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A. (1981) Synthesis of synchronization skeletons for branching time temporal logic. In: Logic of programs, Lecture Notes in Computer Science, vol. 131. Springer, Berlin Heidelberg New York, pp. 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"95_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H. (2000) Counterexample-guided abstraction refinement. In: CAV 00: Computer-aided verification, Lecture Notes in Computer Science, vol. 1885. Springer, Berlin Heidelberg New York,pp. 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"95_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D. (1992) Model checking and abstraction. In: POPL 92: Principles of programming languages. ACM, New York, pp. 343\u2013354","DOI":"10.1145\/143165.143235"},{"key":"95_CR6","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Iyer, P., Yankelevich, D. (1995) Optimality in abstractions of model checking. In: SAS 95: Static analysis, Lecture Notes in Computer Science, vol. 983. Springer, Berlin Heidelberg New York, pp. 51\u201363","DOI":"10.1007\/3-540-60360-3_32"},{"key":"95_CR7","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H. (2000) Bandera: Extracting finite-state models from Java source code. In: ICSE 2000: International Conference on Software Engineering. ACM, New York,pp. 439\u2013448","DOI":"10.1145\/337180.337234"},{"key":"95_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R. (1977) Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: POPL 77: Principles of programming languages. ACM, New York, pp. 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"95_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R. (1995) Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA 95: Functional programming and computer architecture. ACM, New York, pp. 170\u2013181","DOI":"10.1145\/224164.224199"},{"key":"95_CR10","unstructured":"Dams, D., Grumberg, O., Gerth, R. (1994) Abstract interpretation of reactive systems: abstractions preserving ACTL*, ECTL*, and CTL*. In: PROCOMET 94: Programming concepts, methods, and calculi. Elsevier Science, Amsterdam, The Netherlands, pp. 561\u2013581"},{"key":"95_CR11","doi-asserted-by":"crossref","unstructured":"Das, S., Dill, D.L., Park, S. (1999) Experience with predicate abstraction. In: CAV 00: Computer-aided verification, Lecture Notes in Computer Science, vol. 1633. Springer, Berlin Heidelberg New York, pp. 160\u2013171","DOI":"10.1007\/3-540-48683-6_16"},{"key":"95_CR12","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1145\/333979.333989","volume":"47","author":"Giacobazzi,","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F. (2000) Making abstract interpretations complete. J ACM 47(2): 361\u2013416","journal-title":"J ACM"},{"key":"95_CR13","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H. (1997) Construction of abstract state graphs with PVS. In: CAV 97: Computer aided verification, Lecture Notes in Computer Science, vol. 1254. Springer, Berlin Heidelberg New York, pp. 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"95_CR14","doi-asserted-by":"crossref","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.A. (2001) Modal transition systems: a foundation for three-valued program analysis. In: ESOP 01: European symposium on programming. Springer, Berlin Heidelberg New York (to appear)","DOI":"10.1007\/3-540-45309-1_11"},{"key":"95_CR15","doi-asserted-by":"crossref","unstructured":"Kurshan, R. (1994) Computer-aided verification of coordinating processes. Princeton University, Princeton, N.J., USA","DOI":"10.1515\/9781400864041"},{"key":"95_CR16","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"Loiseaux,","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S. (1995) Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst Design 6(1): 11\u201344","journal-title":"Formal Methods Syst Design"},{"key":"95_CR17","doi-asserted-by":"crossref","unstructured":"Podelski, A. (2000) Model checking as constraint solving. In: SAS 00: Static analysis, Lecture Notes in Computer Science, vol. 1824. Springer, Berlin Heidelberg New York, pp. 221\u2013237","DOI":"10.1007\/978-3-540-45099-3_2"},{"key":"95_CR18","doi-asserted-by":"crossref","unstructured":"Reps, T. (1998) Program analysis via graph reachability. Inf Software Technol 40(11-12): 701\u2013726","DOI":"10.1016\/S0950-5849(98)00093-7"},{"key":"95_CR19","doi-asserted-by":"crossref","unstructured":"Reps, T., Horwitz, S., Sagiv, M. (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL 95: Principles of programming languages. ACM, New York,pp. 49\u201361","DOI":"10.1145\/199448.199462"},{"key":"95_CR20","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R. (1999) Parametric shape analysis via 3-valued logic. In: POPL 99: Principles of programming languages. ACM, New York, pp. 105\u2013118","DOI":"10.1145\/292540.292552"},{"key":"95_CR21","doi-asserted-by":"crossref","unstructured":"Sa\u00efdi, H. (2000) Model checking guided abstraction and analysis. In: Palsberg, J. (ed) SAS\u201900: Static analysis, Lecture Notes in Computer Science, vol. 1824. Springer, Berlin Heidelberg New York, pp. 377\u2013396","DOI":"10.1007\/978-3-540-45099-3_20"},{"key":"95_CR22","doi-asserted-by":"crossref","unstructured":"Schmidt, D. (1998) Data flow analysis is model checking of abstract interpretation. In: POPL 98: Principlesof programming languages. ACM, New York, pp.38\u201348","DOI":"10.1145\/268946.268950"},{"key":"95_CR23","unstructured":"Sharir, M., Pnueli, A. (1981) Two approaches to interprocedural data flow analysis. In: Program flow analysis: theory and applications. Prentice-Hall, Englewood Cliffs, N.J., USA,pp. 189\u2013233"},{"key":"95_CR24","doi-asserted-by":"crossref","unstructured":"Steffen, B. (1991) Data flow analysis as model checking. In: TACS 91: Theoretical aspects of computer science, Lecture Notes in Computer Science, vol. 536. Springer, Berlin Heidelberg New York, pp. 346\u2013365","DOI":"10.1007\/3-540-54415-1_54"},{"key":"95_CR25","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/s10009-002-0091-4","volume":"5","author":"Yavuz-Kahveci,","year":"2003","unstructured":"Yavuz-Kahveci, T., Bultan, T. (2003) A symbolic manipulator for automated verification of reactive systems with heterogeneous data types. Int J Softw Tools Technol Tranfer 5(1): 15, 2003","journal-title":"Int J Softw Tools Technol Tranfer"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0095-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0095-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0095-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T18:11:39Z","timestamp":1585678299000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0095-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,10,22]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["95"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0095-0","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,10,22]]}}}