{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:44:35Z","timestamp":1782877475192,"version":"3.54.5"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227515","type":"print"},{"value":"9783032227522","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T00:00:00Z","timestamp":1776297600000},"content-version":"vor","delay-in-days":105,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22752-2_10","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T21:52:07Z","timestamp":1776289927000},"page":"192-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMT(LIA) Sampling with High Diversity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6882-0107","authenticated-orcid":false,"given":"Yong","family":"Lai","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3751-9281","authenticated-orcid":false,"given":"Junjie","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5028-1064","authenticated-orcid":false,"given":"Chuan","family":"Luo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,16]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442 (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"10_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329 (2021)","DOI":"10.3233\/FAIA201017"},{"key":"10_CR4","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008. pp. 209\u2013224 (2008)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cai, S., Li, B., Zhang, X.: Local search for SMT on linear integer arithmetic. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022. Lecture Notes in Computer Science, vol. 13372, pp. 227\u2013248 (2022)","DOI":"10.1007\/978-3-031-13188-2_12"},{"key":"10_CR6","unstructured":"Cai, S., Su, K.: Local search for boolean satisfiability with configuration checking and subscore. Artificial Intelligence"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Carrasco, M., Cadar, C., Donaldson, A.: Scalable smt sampling for floating-point formulas via coverage-guided fuzzing. In: IEEE International Conference on Software Testing, Verification, and Validation (ICST 2025) (2025)","DOI":"10.1109\/ICST62969.2025.10989031"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathsat5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Lecture Notes in Computer Science, vol.\u00a07795, pp. 93\u2013107 (2013)","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"10_CR9","unstructured":"Codish, M., Fekete, Y., Fuhs, C., Giesl, J., Waldmann, J.: Exotic semi-ring constraints. In: Fontaine, P., Goel, A. (eds.) 10th International Workshop on Satisfiability Modulo Theories, SMT 2012. EPiC Series in Computing, vol.\u00a020, pp. 88\u201397 (2012)"},{"key":"10_CR10","unstructured":"Dutra, R., Bachrach, J., Sen, K.: Smtsampler: efficient stimulus generation from complex SMT constraints. In: Bahar, I. (ed.) Proceedings of the International Conference on Computer-Aided Design, ICCAD 2018. p.\u00a030 (2018)"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Dutra, R., Bachrach, J., Sen, K.: GUIDEDSAMPLER: coverage-guided sampling of SMT solutions. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019. pp. 203\u2013211 (2019)","DOI":"10.23919\/FMCAD.2019.8894251"},{"key":"10_CR12","unstructured":"Ermon, S., Gomes, C.P., Sabharwal, A., Selman, B.: Embed and project: Discrete sampling with universal hashing. In: Burges, C.J.C., Bottou, L., Ghahramani, Z., Weinberger, K.Q. (eds.) Advances in Neural Information Processing Systems 26: 27th Annual Conference on Neural Information Processing Systems 2013. pp. 2085\u20132093 (2013)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C.M., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. pp. 1136\u20131143 (2015)","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL( T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) Computer Aided Verification, 16th International Conference, CAV 2004. Lecture Notes in Computer Science, vol.\u00a03114, pp. 175\u2013188 (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Gavrilenko, N., de\u00a0Le\u00f3n, H.P., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: Relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019. Lecture Notes in Computer Science, vol. 11561, pp. 355\u2013365 (2019)","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation. pp. 213\u2013223 (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"10_CR17","unstructured":"Golia, P., Soos, M., Chakraborty, S., Meel, K.S.: Designing samplers is easy: The boon of testers. In: Formal Methods in Computer Aided Design, FMCAD 2021. pp. 222\u2013230 (2021)"},{"key":"10_CR18","unstructured":"Holler, C., Herzig, K., Zeller, A.: Fuzzing with code fragments. In: Kohno, T. (ed.) Proceedings of the 21th USENIX Security Symposium. pp. 445\u2013458 (2012)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Huang, H., Yao, P., Wu, R., Shi, Q., Zhang, C.: Pangolin: Incremental hybrid fuzzing with polyhedral path abstraction. In: 2020 IEEE Symposium on Security and Privacy, SP 2020. pp. 1613\u20131627 (2020)","DOI":"10.1109\/SP40000.2020.00063"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Jiang, L., Yuan, H., Wu, M., Zhang, L., Zhang, Y.: Evaluating and improving hybrid fuzzing. In: 45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023. pp. 410\u2013422 (2023)","DOI":"10.1109\/ICSE48619.2023.00045"},{"key":"10_CR21","unstructured":"Kitchen, N.: Markov Chain Monte Carlo Stimulus Generation for Constrained Random Simulation. Ph.D. thesis, University of California, Berkeley, USA (2010)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Kitchen, N., Kuehlmann, A.: Stimulus generation for constrained random simulation. In: Gielen, G.G.E. (ed.) 2007 International Conference on Computer-Aided Design, ICCAD 2007. pp. 258\u2013265 (2007)","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series, Springer (2016)","DOI":"10.1007\/978-3-662-50497-0"},{"key":"10_CR24","unstructured":"Lai, Y., Li, J., Luo, C.: SMT(LIA) sampling with high diversity. arXiv preprint arXiv:2503.04782 (2025)"},{"key":"10_CR25","first-page":"453","volume":"58","author":"Y Lai","year":"2017","unstructured":"Lai, Y., Liu, D., Yin, M.: New canonical representations by augmenting obdds with conjunctive decomposition. 58, 453\u2013521 (2017)","journal-title":"New canonical representations by augmenting obdds with conjunctive decomposition."},{"key":"10_CR26","unstructured":"Lai, Y., Meel, K.S., Yap, R.H.: Panini: an efficient and flexible knowledge compiler. In: International Conference on Computer Aided Verification. pp. 92\u2013105. Springer (2025)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Liu, C., Liu, G., Luo, C., Cai, S., Lei, Z., Zhang, W., Chu, Y., Zhang, G.: Optimizing local search-based partial maxsat solving via initial assignment prediction. Sci. China Inf. Sci. 68(2) (2025)","DOI":"10.1007\/s11432-023-3900-7"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Liu, D., Ernst, G., Murray, T., Rubinstein, B.I.P.: LEGION: best-first concolic testing. In: 35th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2020. pp. 54\u201365 (2020)","DOI":"10.1145\/3324884.3416629"},{"issue":"4","key":"10_CR29","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/s10009-015-0366-1","volume":"18","author":"NP Lopes","year":"2016","unstructured":"Lopes, N.P., Monteiro, J.: Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic. Int. J. Softw. Tools Technol. Transf. 18(4), 359\u2013374 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Luo, C., Song, J., Zhao, Q., Sun, B., Chen, J., Zhang, H., Lin, J., Hu, C.: Solving the t-wise coverage maximum problem via effective and efficient local search-based sampling. ACM Trans. Softw. Eng. Methodol. 34(1), 13:1\u201313:64 (2025)","DOI":"10.1145\/3688836"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Luo, C., Sun, B., Qiao, B., Chen, J., Zhang, H., Lin, J., Lin, Q., Zhang, D.: Ls-sampling: an effective local search based sampling approach for achieving high t-wise coverage. In: Spinellis, D., Gousios, G., Chechik, M., Penta, M.D. (eds.) ESEC\/FSE \u201921: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. pp. 1081\u20131092 (2021)","DOI":"10.1145\/3468264.3468622"},{"key":"10_CR32","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, pp. 21\u201328 (1962)"},{"key":"10_CR33","unstructured":"Meel, K.S.: Sampling techniques for boolean satisfiability. CoRR abs\/1404.6682 (2014)"},{"key":"10_CR34","unstructured":"Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: Universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP, Papers from the 2016 AAAI Workshop. AAAI Technical Report, vol. WS-16-05 (2016)"},{"key":"10_CR35","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual Design Automation Conference. pp. 530\u2013535 (2001)"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Nadel, A.: Generating diverse solutions in sat. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 287\u2013301. Springer (2011)","DOI":"10.1007\/978-3-642-21581-0_23"},{"key":"10_CR38","unstructured":"Naveh, Y., Rimon, M., Jaeger, I., Katz, Y., Vinov, M., Marcus, E., Shurek, G.: Constraint-based random stimuli generation for hardware verification pp. 1720\u20131727 (2006)"},{"key":"10_CR39","doi-asserted-by":"crossref","unstructured":"Peled, M., Rothenberg, B., Itzhaky, S.: SMT sampling via model-guided approximation. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th International Symposium, FM 2023. Lecture Notes in Computer Science, vol. 14000, pp. 74\u201391 (2023)","DOI":"10.1007\/978-3-031-27481-7_6"},{"key":"10_CR40","doi-asserted-by":"crossref","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with smt-solving and abstract interpretation. In: Bobaru, M.G., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods - Third International Symposium, NFM 2011. Lecture Notes in Computer Science, vol.\u00a06617, pp. 298\u2013312 (2011)","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"10_CR41","doi-asserted-by":"crossref","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: International conference on theory and applications of satisfiability testing. pp. 294\u2013299. Springer (2007)","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"10_CR42","unstructured":"Poeplau, S., Francillon, A.: Symbolic execution with symcc: Don\u2019t interpret, compile! In: Capkun, S., Roesner, F. (eds.) 29th USENIX Security Symposium, USENIX Security 2020. pp. 181\u2013198 (2020)"},{"key":"10_CR43","doi-asserted-by":"crossref","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: Wermelinger, M., Gall, H.C. (eds.) Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005. pp. 263\u2013272 (2005)","DOI":"10.1145\/1081706.1081750"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"Sharma, S., Gupta, R., Roy, S., Meel, K.S.: Knowledge compilation meets uniform sampling. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a057, pp. 620\u2013636 (2018)","DOI":"10.29007\/h4p9"},{"key":"10_CR45","unstructured":"Shaw, A., Meel, K.S.: CSB: A counting and sampling tool for bit-vectors. In: Reger, G., Zohar, Y. (eds.) Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories co-located with the 36th International Conference on Computer Aided Verification (CAV 2024). CEUR Workshop Proceedings, vol.\u00a03725, pp. 36\u201343 (2024)"},{"key":"10_CR46","unstructured":"Thornton, J., Pham, D.N., Bain, S., Ferreira\u00a0Jr, V.: Additive versus multiplicative clause weighting for sat. In: AAAI. vol.\u00a04, pp. 191\u2013196 (2004)"},{"key":"10_CR47","doi-asserted-by":"crossref","unstructured":"Zhang, X., Li, B., Cai, S.: Deep combination of CDCL(T) and local search for satisfiability modulo non-linear integer arithmetic theory. In: Proceedings of the 46th IEEE\/ACM International Conference on Software Engineering, ICSE 2024. pp. 125:1\u2013125:13 (2024)","DOI":"10.1145\/3597503.3639105"},{"key":"10_CR48","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Chen, Z., Shuai, Z., Zhang, T., Li, K., Wang, J.: Multiplex symbolic execution: Exploring multiple paths by solving once. In: Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering. pp. 846\u2013857 (2020)","DOI":"10.1145\/3324884.3416645"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22752-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T02:46:30Z","timestamp":1782873990000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22752-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227515","9783032227522"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22752-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"16 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}