{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T12:52:17Z","timestamp":1794401537975,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642246890","type":"print"},{"value":"9783642246906","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_11","type":"book-chapter","created":{"date-parts":[[2011,10,24]],"date-time":"2011-10-24T21:35:37Z","timestamp":1319492137000},"page":"138-154","source":"Crossref","is-referenced-by-count":6,"title":["A Dataflow Analysis to Improve SAT-Based Bounded Program Verification"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Cuervo Parrino","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Juan Pablo","family":"Galeotti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA 2002, pp. 123\u2013133 (2002)","DOI":"10.1145\/566172.566191"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Belt J., Robby, Deng X.: Sireum\/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses. In: FSE 2009, pp. 355\u2013364 (2009)","DOI":"10.1145\/1595696.1595762"},{"key":"11_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185 (2009)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Cuervo Parrino, B., Galeotti, J.P., Garbervetsky, D., Frias, M.: A dataflow analysis to improve SAT-based program verification, Technical Report (May 2011), http:\/\/www.dc.uba.ar\/tacoflow\/techrep.pdf","DOI":"10.1007\/978-3-642-24690-6_11"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM TOPLAS\u00a013(4), 451\u2013490","DOI":"10.1145\/115372.115320"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P. Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond Assertions: Advanced Specification and Verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 342\u2013363. Springer, Heidelberg (2006)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-87873-5_13","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Dennis","year":"2008","unstructured":"Dennis, G., Yessenov, K., Jackson, D.: Bounded Verification of Voting Software. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 130\u2013145. Springer, Heidelberg (2008)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Frias, M.F., Galeotti, J.P., Lopez Pombo, C.G., Aguirre, N.: DynAlloy: Upgrading Alloy with Actions. In: ICSE 2005, pp. 442\u2013450 (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"11_CR9","unstructured":"Galeotti, J.: Software Verification Using Alloy. PhD. Thesis, UBA (2011)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C.G., Frias, M.F.: Analysis of invariants for efficient bounded verification. In: Proceedings of ISSTA 2010, pp. 25\u201336 (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"11_CR11","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic. Foundations of Computing","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. Foundations of Computing. MIT Press, Cambridge (2000)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"11_CR13","volume-title":"Software Abstractions","author":"D. Jackson","year":"2006","unstructured":"Jackson, D.: Software Abstractions. MIT Press, Cambridge (2006)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA 2000, pp. 14\u201325 (2000)","DOI":"10.1145\/347324.383378"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Kindall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194\u2013206 (1973)","DOI":"10.1145\/512927.512945"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00263194","volume":"18","author":"F. Nielson","year":"1982","unstructured":"Nielson, F.: A denotational framework for data flow analysis. Acta Inf.\u00a018, 265\u2013287 (1982)","journal-title":"Acta Inf."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Shao, D., Gopinath, D., Khurshid, S., Perry, D.E.: Optimizing Incremental Scope-Bounded Checking with Data-Flow Analysis. In: ISSRE 2010, pp. 408\u2013417 (2010)","DOI":"10.1109\/ISSRE.2010.27"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-19811-3_19","volume-title":"Fundamental Approaches to Software Engineering","author":"R. Sharma","year":"2011","unstructured":"Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D.: Testing Container Classes: Random or Systematic? In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol.\u00a06603, pp. 262\u2013277. Springer, Heidelberg (2011)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-10373-5_5","volume-title":"Formal Methods and Software Engineering","author":"J.H. Siddiqui","year":"2009","unstructured":"Siddiqui, J.H., Khurshid, S.: An Empirical Study of Structural Constraint Solving Techniques. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 88\u2013106. Springer, Heidelberg (2009)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"632","DOI":"10.1007\/978-3-540-71209-1_49","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Torlak","year":"2007","unstructured":"Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 632\u2013647. Springer, Heidelberg (2007)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Taghdiri, M., Seater, R., Jackson, D.: Lightweight extraction of Syntactic Specifications. In: FSE 2006, pp. 276\u2013286 (2006)","DOI":"10.1145\/1181775.1181809"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u0103s\u0103reanu, C.S., Pel\u00e1nek, R.: Test Input Generation for Java Containers using State Matching. In: ISSTA 2006, pp. 37\u201348 (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: A scalable framework for error detection using Boolean satisfiability. ACM TOPLAS\u00a029(3) (2007)","DOI":"10.1145\/1232420.1232423"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T03:09:49Z","timestamp":1741835389000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_11","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}