{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:08:20Z","timestamp":1770271700782,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":58,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T00:00:00Z","timestamp":1503273600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,8,21]]},"DOI":"10.1145\/3106237.3106303","type":"proceedings-article","created":{"date-parts":[[2017,8,2]],"date-time":"2017-08-02T19:36:18Z","timestamp":1501702578000},"page":"535-546","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Constraint normalization and parameterized caching for quantitative program analysis"],"prefix":"10.1145","author":[{"given":"Tegan","family":"Brennan","sequence":"first","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"given":"Nestan","family":"Tsiskaridze","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"given":"Nicol\u00e1s","family":"Rosner","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"given":"Abdulbaki","family":"Aydin","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]},{"given":"Tevfik","family":"Bultan","sequence":"additional","affiliation":[{"name":"University of California at Santa Barbara, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,8,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Redis. https:\/\/redis.io\/.  Redis. https:\/\/redis.io\/."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.75"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771802"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.46"},{"key":"e_1_3_2_1_6_1","first-page":"272","volume-title":"CAV 2015, San Francisco, CA, USA, Proceedings, Part I","author":"Aydin A.","year":"2015","unstructured":"A. Aydin , L. Bang , and T. Bultan . Automata-based model counting for string constraints. In Computer Aided Verification - 27th International Conference , CAV 2015, San Francisco, CA, USA, Proceedings, Part I , pages 255\u2013 272 , 2015 . A. Aydin, L. Bang, and T. Bultan. Automata-based model counting for string constraints. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, Proceedings, Part I, pages 255\u2013272, 2015."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2009.18"},{"key":"e_1_3_2_1_8_1","unstructured":"V. Baldoni N. Berline J. D. Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. Latte integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/ 2004.  V. Baldoni N. Berline J. D. Loera B. Dutra M. K\u00f6ppe S. Moreinis G. Pinto M. Vergne and J. Wu. Latte integrale v1.7.2. http:\/\/www.math.ucdavis.edu\/ latte\/ 2004."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_3_2_1_10_1","first-page":"3","volume-title":"Haifa Verification Conference","author":"Barrett C.","unstructured":"C. Barrett , L. de Moura , S. Ranise , A. Stump , and C. Tinelli . The smt-lib initiative and the rise of smt . In Haifa Verification Conference , pages 3\u2013 3 . Springer, 2010. C. Barrett, L. de Moura, S. Ranise, A. Stump, and C. Tinelli. The smt-lib initiative and the rise of smt. In Haifa Verification Conference, pages 3\u20133. Springer, 2010."},{"key":"e_1_3_2_1_11_1","unstructured":"ESEC\/FSE\u201917 September 4\u20138 2017 Paderborn Germany T. Brennan N. Tsiskaridze N. Rosner S. Aydin and T. Bultan  ESEC\/FSE\u201917 September 4\u20138 2017 Paderborn Germany T. Brennan N. Tsiskaridze N. Rosner S. Aydin and T. Bultan"},{"key":"e_1_3_2_1_12_1","first-page":"177","volume-title":"International Conference on Computer Aided Verification","author":"Barrett C.","unstructured":"C. Barrett , C. L. Conway , M. Deters , L. Hadarean , D. Jovanovi\u0107 , T. King , A. Reynolds , and C. Tinelli . Cvc4 . In International Conference on Computer Aided Verification , pages 171\u2013 177 . Springer, 2011. C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovi\u0107, T. King, A. Reynolds, and C. Tinelli. Cvc4. In International Conference on Computer Aided Verification, pages 171\u2013177. Springer, 2011."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9246-5"},{"key":"e_1_3_2_1_14_1","volume-title":"Department of Computer Science","author":"Barrett C.","year":"2015","unstructured":"C. Barrett , P. Fontaine , and C. Tinelli . The SMT-LIB Standard: Version 2.5. Technical report , Department of Computer Science , The University of Iowa , 2015 . Available at www.smt-lib.org. C. Barrett, P. Fontaine, and C. Tinelli. The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa, 2015. Available at www.smt-lib.org."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786832"},{"key":"e_1_3_2_1_16_1","first-page":"224","volume-title":"8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. R. Engler . KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs . In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA , Proceedings , pages 209\u2013 224 , 2008 . C. Cadar, D. Dunbar, and D. R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pages 209\u2013224, 2008."},{"key":"e_1_3_2_1_17_1","volume-title":"Approximate probabilistic inference via word-level counting. arXiv preprint arXiv:1511.07663","author":"Chakraborty S.","year":"2015","unstructured":"S. Chakraborty , K. S. Meel , R. Mistry , and M. Y. Vardi . Approximate probabilistic inference via word-level counting. arXiv preprint arXiv:1511.07663 , 2015 . S. Chakraborty, K. S. Meel, R. Mistry, and M. Y. Vardi. Approximate probabilistic inference via word-level counting. arXiv preprint arXiv:1511.07663, 2015."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1370628.1370629"},{"key":"e_1_3_2_1_19_1","volume-title":"AAAI Workshop on Tractable Reasoning. Citeseer","author":"Crawford J.","year":"1992","unstructured":"J. Crawford . A theoretical analysis of reasoning by symmetry in first-order logic . In AAAI Workshop on Tractable Reasoning. Citeseer , 1992 . J. Crawford. A theoretical analysis of reasoning by symmetry in first-order logic. In AAAI Workshop on Tractable Reasoning. Citeseer, 1992."},{"key":"e_1_3_2_1_20_1","first-page":"148","article-title":"Symmetry-breaking predicates for search problems","volume":"96","author":"Crawford J.","year":"1996","unstructured":"J. Crawford , M. Ginsberg , E. Luks , and A. Roy . Symmetry-breaking predicates for search problems . KR , 96 : 148 \u2013 159 , 1996 . J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. KR, 96:148\u2013159, 1996.","journal-title":"KR"},{"key":"e_1_3_2_1_21_1","first-page":"340","volume-title":"International conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"De Moura L.","unstructured":"L. De Moura and N. Bj\u00f8rner . Z3: An efficient smt solver . In International conference on Tools and Algorithms for the Construction and Analysis of Systems , pages 337\u2013 340 . Springer, 2008. L. De Moura and N. Bj\u00f8rner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337\u2013 340. Springer, 2008."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486870"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_3_2_1_26_1","volume-title":"Citeseer","author":"Gent I. P.","year":"1999","unstructured":"I. P. Gent and B. Smith . Symmetry breaking during search in constraint programming . Citeseer , 1999 . I. P. Gent and B. Smith. Symmetry breaking during search in constraint programming. Citeseer, 1999."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1574-6526(06)80014-3"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1920261.1920300"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542498"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859080"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_2_1_33_1","first-page":"568","volume-title":"9th International Conference, TACAS 2003, Warsaw, Poland, April 7-11, 2003","author":"Khurshid S.","year":"2003","unstructured":"S. Khurshid , C. S. Pasareanu , and W. Visser . Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems , 9th International Conference, TACAS 2003, Warsaw, Poland, April 7-11, 2003 , Proceedings , pages 553\u2013 568 , 2003 . S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference, TACAS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pages 553\u2013568, 2003."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0247-6"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.04.003"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2643011"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594331"},{"key":"e_1_3_2_1_41_1","first-page":"559","volume-title":"Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design","author":"Mao B.","unstructured":"B. Mao , W. Hu , A. Althoff , J. Matai , J. Oberg , D. Mu , T. Sherwood , and R. Kastner . Quantifying timing-based information flow in cryptographic hardware . In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design , pages 552\u2013 559 . IEEE Press, 2015. B. Mao, W. Hu, A. Althoff, J. Matai, J. Oberg, D. Mu, T. Sherwood, and R. Kastner. Quantifying timing-based information flow in cryptographic hardware. In Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, pages 552\u2013559. IEEE Press, 2015."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375606"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382791"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2632362.2632367"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2590296.2590328"},{"key":"e_1_3_2_1_47_1","volume-title":"Ekoparty Security Conference","author":"Rizzo J.","year":"2012","unstructured":"J. Rizzo and T. Duong . The crime attack . Ekoparty Security Conference , 2012 . J. Rizzo and T. Duong. The crime attack. Ekoparty Security Conference, 2012."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0653(04)00311-7"},{"key":"e_1_3_2_1_51_1","first-page":"302","volume-title":"12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings","author":"Smith G.","year":"2009","unstructured":"G. Smith . On the foundations of quantitative information flow. In Foundations of Software Science and Computational Structures , 12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings , pages 288\u2013 302 , 2009 . G. Smith. On the foundations of quantitative information flow. In Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, York, UK, March 22-29, 2009. Proceedings, pages 288\u2013302, 2009."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_38"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_1_54_1","first-page":"46","volume-title":"2016 IEEE European Symposium on","author":"Val C. G.","unstructured":"C. G. Val , M. A. Enescu , S. Bayless , W. Aiello , and A. J. Hu . Precisely measuring quantitative information flow: 10k lines of code and beyond. In Security and Privacy (EuroS&P) , 2016 IEEE European Symposium on , pages 31\u2013 46 . IEEE, 2016. C. G. Val, M. A. Enescu, S. Bayless, W. Aiello, and A. J. Hu. Precisely measuring quantitative information flow: 10k lines of code and beyond. In Security and Privacy (EuroS&P), 2016 IEEE European Symposium on, pages 31\u201346. IEEE, 2016."},{"key":"e_1_3_2_1_55_1","volume-title":"Electronically","author":"Verdoolaege S.","year":"2007","unstructured":"S. Verdoolaege . barvinok: User guide. Version 0.23) , Electronically available at http:\/\/www. kotnet. org\/\u02dc skimo\/barvinok, 2007 . S. Verdoolaege. barvinok: User guide. Version 0.23), Electronically available at http:\/\/www. kotnet. org\/\u02dc skimo\/barvinok, 2007."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866327"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"ESEC\/FSE'17: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering","location":"Paderborn Germany","acronym":"ESEC\/FSE'17","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3106237.3106303","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:37Z","timestamp":1750217437000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3106237.3106303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,21]]},"references-count":58,"alternative-id":["10.1145\/3106237.3106303","10.1145\/3106237"],"URL":"https:\/\/doi.org\/10.1145\/3106237.3106303","relation":{},"subject":[],"published":{"date-parts":[[2017,8,21]]},"assertion":[{"value":"2017-08-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}