{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T16:19:02Z","timestamp":1673108342299},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,2,25]],"date-time":"2014-02-25T00:00:00Z","timestamp":1393286400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-014-0401-9","type":"journal-article","created":{"date-parts":[[2014,2,24]],"date-time":"2014-02-24T06:53:30Z","timestamp":1393224810000},"page":"45-63","source":"Crossref","is-referenced-by-count":2,"title":["TacoFlow: optimizing SAT program verification using dataflow analysis"],"prefix":"10.1007","volume":"14","author":[{"given":"Bruno","family":"Cuervo\u00a0Parrino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Juan Pablo","family":"Galeotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Diego","family":"Garbervetsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,25]]},"reference":[{"key":"401_CR1","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 1\u201311. ACM (1988)","DOI":"10.1145\/73560.73561"},{"key":"401_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: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The foundations of software engineering, pp. 355\u2013364. ACM (2009)","DOI":"10.1145\/1595696.1595762"},{"key":"401_CR3","unstructured":"Biere, A.: Pre,icoSAT@SC\u201909. Solver description for sat competition 2009. In: In SAT 2009 Competitive Event Booklet (2009)"},{"key":"401_CR4","volume-title":"Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications","author":"A Biere","year":"2009","unstructured":"Biere, A., Biere, A., Heule, M., van Maaren, H., Walsh, T.: Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam (2009)"},{"key":"401_CR5","doi-asserted-by":"crossref","unstructured":"Blanc, N., Kroening, D., Sharygina, N.: Scoot: A tool for the analysis of SystemC models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol. 4963, pp. 467\u2013470 (2008)","DOI":"10.1007\/978-3-540-78800-3_36"},{"key":"401_CR6","doi-asserted-by":"crossref","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on java predicates. In: Proceedings of the 2002 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 123\u2013133. ACM (2002)","DOI":"10.1145\/566171.566191"},{"key":"401_CR7","doi-asserted-by":"crossref","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with jml and esc\/java2. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects, pp. 342\u2013363. Springer (2006)","DOI":"10.1007\/11804192_16"},{"key":"401_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ansi-c programs. In: In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), LNCS, vol. 2988, pp. 168\u2013176. Springer (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"401_CR9","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Lecture Notes in Computer Science, vol. 3440, pp. 570\u2013574. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"401_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 269\u2013282. ACM (1979)","DOI":"10.1145\/567752.567778"},{"issue":"2\u20133","key":"401_CR11","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/0743-1066(92)90030-7","volume":"13","author":"P Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2\u20133), 103\u2013179 (1992)","journal-title":"J. Log. Program."},{"key":"401_CR12","unstructured":"Crawford, J., Ginsberg, M., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: Principles of Knowledge Representation and Reasoning, pp. 148\u2013159 (1996)"},{"key":"401_CR13","doi-asserted-by":"crossref","unstructured":"Dennis, G., Yessenov, K., Jackson, D.: Bounded verification of voting software. In: Proceedings of the 2nd International Conference on Verified Software: Theories, Tools, Experiments, pp. 130\u2013145. Springer (2008)","DOI":"10.1007\/978-3-540-87873-5_13"},{"key":"401_CR14","doi-asserted-by":"crossref","unstructured":"Dolby, J., Vaziri, M., Tip, F.: Finding bugs efficiently with a sat solver. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE \u201907, pp. 95\u2013204, New York, NY, USA, ACM (2007)","DOI":"10.1145\/1287624.1287653"},{"key":"401_CR15","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A., (eds.), SAT, Lecture Notes in Computer Science, vol. 2919, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"401_CR16","doi-asserted-by":"crossref","unstructured":"Frias, M., Galeotti, J.P., L\u00f3pez Pombo, C., Aguirre, N. Dynalloy: upgrading alloy with actions. In: Proceedings of the 27th International Conference on Software Engineering, pp. 442\u2013451. ACM (2005)","DOI":"10.1145\/1062455.1062535"},{"key":"401_CR17","unstructured":"Galeotti, J.P.: Software Verification Using Alloy. PhD thesis, University of Buenos Aires (2010)"},{"key":"401_CR18","doi-asserted-by":"crossref","unstructured":"Galeotti, J.P., Rosner, N., L\u00f3pez Pombo, C., Frias, M.: Analysis of invariants for efficient bounded verification. In: Proceedings of the 19th International Symposium on Software Testing and Analysis, pp. 25\u201336. ACM (2010)","DOI":"10.1145\/1831708.1831712"},{"key":"401_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Jerzy, T.: Dynamic Logic. The MIT Press, Cambridge (2000)"},{"key":"401_CR20","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-soft: Software verification platform. In CAV\u201905, pp. 301\u2013306 (2005)","DOI":"10.1007\/11513988_31"},{"issue":"2","key":"401_CR21","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"401_CR22","volume-title":"Software Abstractions: Logic, Language, and Analysis (Revised Edition)","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language, and Analysis (Revised Edition). The MIT Press, Cambridge (2012)"},{"key":"401_CR23","doi-asserted-by":"crossref","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proceedings of the 2000 ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 14\u201325. ACM (2000)","DOI":"10.1145\/347636.383378"},{"key":"401_CR24","doi-asserted-by":"crossref","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 194\u2013206. ACM (1973)","DOI":"10.1145\/512927.512945"},{"key":"401_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)"},{"key":"401_CR26","first-page":"265","volume":"18","author":"Flemming Nielson","year":"1982","unstructured":"Nielson, Flemming: A denotational framework for data flow analysis. Acta Inform. 18, 265\u2013287 (1982)","journal-title":"Acta Inform."},{"issue":"2","key":"401_CR27","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1002\/stvr.399","volume":"19","author":"H Post","year":"2009","unstructured":"Post, H., Sinz, C., K\u00fcchlin, W.: Towards automatic software model checking of thousands of linux modules\u2014a case study with avinux. Softw. Test. Verif. Reliab. 19(2), 155\u2013172 (2009)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"401_CR28","doi-asserted-by":"crossref","unstructured":"Shao, D., Gopinath, D., Khurshid, S., Perry, D.E.: Optimizing incremental scope-bounded checking with data-flow analysis. In: Proceedings of the 2010 IEEE 21st International Symposium on Software Reliability Engineering, pp. 408\u2013417. IEEE Computer Society (2010)","DOI":"10.1109\/ISSRE.2010.27"},{"key":"401_CR29","doi-asserted-by":"crossref","unstructured":"Sharma, R., Gligoric, M., Arcuri, A., Fraser, G., Marinov, D.: Testing container classes: random or systematic? In: Proceedings of the 14th International Conference on Fundamental Approaches to Software Engineering: Part of the Joint European Conferences on Theory and Practice of Software, FASE\u201911\/ETAPS\u201911, pp. 262\u2013277. Springer (2011)","DOI":"10.1007\/978-3-642-19811-3_19"},{"key":"401_CR30","doi-asserted-by":"crossref","unstructured":"Siddiqui, J.H., Khurshid, S.: An empirical study of structural constraint solving techniques. In: Proceedings of the 11th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, pp. 88\u2013106. Springer (2009)","DOI":"10.1007\/978-3-642-10373-5_5"},{"key":"401_CR31","doi-asserted-by":"crossref","unstructured":"Taghdiri, M., Seater, R., Jackson, D.: Lightweight extraction of syntactic specifications. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 276\u2013286. ACM (2006)","DOI":"10.1145\/1181775.1181809"},{"key":"401_CR32","doi-asserted-by":"crossref","unstructured":"Torlak, E., Jackson, E.: Kodkod: a relational model finder. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 632\u2013647. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"401_CR33","doi-asserted-by":"crossref","unstructured":"Visser, W., P\u01ces\u01cereanu, C.S., Pel\u00e1nek, R.: Test input generation for java containers using state matching. In: Proceedings of the 2006 International Symposium on Software Testing and Analysis, pp. 37\u201348. ACM (2006)","DOI":"10.1145\/1146238.1146243"},{"key":"401_CR34","doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Saturn: a scalable framework for error detection using boolean satisfiability. ACM Trans. Program. Lang. Syst. 29, 16-es (2007)","DOI":"10.1145\/1232420.1232423"},{"key":"401_CR35","unstructured":"Yessenov, K.: A light-weight specification language for bounded program verification. Master\u2019s thesis, MIT (2009)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0401-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-014-0401-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0401-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T22:23:23Z","timestamp":1565216603000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-014-0401-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,25]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["401"],"URL":"https:\/\/doi.org\/10.1007\/s10270-014-0401-9","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2,25]]}}}