{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T04:35:04Z","timestamp":1771043704507,"version":"3.50.1"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030176006","type":"print"},{"value":"9783030176013","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17601-3_4","type":"book-chapter","created":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T19:24:23Z","timestamp":1555442663000},"page":"148-201","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Programming Z3"],"prefix":"10.1007","author":[{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"first","affiliation":[]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[]},{"given":"Lev","family":"Nachmanson","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0102-4381","authenticated-orcid":false,"given":"Christoph M.","family":"Wintersteiger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,14]]},"reference":[{"issue":"5\u20136","key":"4_CR1","first-page":"708","volume":"17","author":"M Alviano","year":"2017","unstructured":"Alviano, M.: Model enumeration in propositional circumscription via unsatisfiable core analysis. TPLP 17(5\u20136), 708\u2013725 (2017)","journal-title":"TPLP"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-33954-2_3","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"F Bacchus","year":"2016","unstructured":"Bacchus, F., Katsirelos, G.: Finding a collection of MUSes incrementally. In: Quimper, C.-G. (ed.) CPAIOR 2016. LNCS, vol. 9676, pp. 35\u201344. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33954-2_3"},{"key":"4_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457\u2013481. IOS Press (2009). https:\/\/doi.org\/10.3233\/978-1-58603-929-5-457","DOI":"10.3233\/978-1-58603-929-5-457"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-23534-9_2","volume-title":"Fields of Logic and Computation II","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24\u201351. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"4_CR6","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with alternating quantifier satisfaction. In: LPAR Short Presentation Papers (2015)"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N., Nachmanson, L.: Theorem recycling for theorem proving. In: Kov\u00e1cs, L., Voronkov, A. (eds.) Vampire 2017, Proceedings of the 4th Vampire Workshop. EPiC Series in Computing, vol. 53, pp. 1\u20138. EasyChair (2018). https:\/\/doi.org\/10.29007\/r58f, https:\/\/easychair.org\/publications\/paper\/qGfG","DOI":"10.29007\/r58f"},{"issue":"2","key":"4_CR8","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reason."},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer-Aided Design, 7th International Conference, FMCAD 2007, Austin, Texas, USA, 11\u201314 November 2007, Proceedings, pp. 173\u2013180 (2007). https:\/\/doi.org\/10.1109\/FAMCAD.2007.15","DOI":"10.1109\/FAMCAD.2007.15"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Lecture Notes in Computer Science","author":"Aaron R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, 8\u201310 January 2006, Proceedings, pp. 427\u2013442 (2006). https:\/\/doi.org\/10.1007\/11609773_28"},{"issue":"3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10703-017-0278-7","volume":"51","author":"M Bromberger","year":"2017","unstructured":"Bromberger, M., Weidenbach, C.: New techniques for linear arithmetic: cubes and equalities. Form. Methods Syst. Des. 51(3), 433\u2013461 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0278-7","journal-title":"Form. Methods Syst. Des."},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-39611-3_12","volume-title":"Hardware and Software: Verification and Testing","author":"H Chockler","year":"2013","unstructured":"Chockler, H., Ivrii, A., Matsliah, A.: Computing interpolants without proofs. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 72\u201385. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_12"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-319-21668-3_3","volume-title":"Computer Aided Verification","author":"J Christ","year":"2015","unstructured":"Christ, J., Hoenicke, J.: Cutting the mix. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 37\u201352. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_3"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-94144-8_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Cimatti","year":"2018","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383\u2013398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_23"},{"issue":"6","key":"4_CR15","doi-asserted-by":"publisher","first-page":"1313","DOI":"10.1137\/S0097539791256325","volume":"23","author":"E Cohen","year":"1994","unstructured":"Cohen, E., Megiddo, N.: Improved algorithms for linear inequalities with two variables per inequality. SIAM J. Comput. 23(6), 1313\u20131347 (1994). https:\/\/doi.org\/10.1137\/S0097539791256325","journal-title":"SIAM J. Comput."},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-45349-0_14","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2000","author":"A Colmerauer","year":"2000","unstructured":"Colmerauer, A., Dao, T.-B.-H.: Expressiveness of full first order constraints in the algebra of finite or infinite trees. In: Dechter, R. (ed.) CP 2000. LNCS, vol. 1894, pp. 172\u2013186. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-45349-0_14"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/11513988_46","volume-title":"Computer Aided Verification","author":"A Costan","year":"2005","unstructured":"Costan, A., Gaubert, S., Goubault, E., Martel, M., Putot, S.: A policy iteration algorithm for computing fixed points in static analysis of programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 462\u2013475. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_46"},{"key":"4_CR18","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233\u2013247. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_20"},{"issue":"4","key":"4_CR20","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"PJ Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758\u2013771 (1980). https:\/\/doi.org\/10.1145\/322217.322228","journal-title":"J. ACM"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2012, Beijing, China, 11\u201316 June 2012, pp. 405\u2013416 (2012). https:\/\/doi.org\/10.1145\/2254064.2254112","DOI":"10.1145\/2254064.2254112"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127\u2013168 (2015). https:\/\/doi.org\/10.1613\/jair.4694","journal-title":"J. Artif. Intell. Res."},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-31612-8_13","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"K Hoder","year":"2012","unstructured":"Hoder, K., Bj\u00f8rner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157\u2013171. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_13"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-642-22110-1_36","volume-title":"Computer Aided Verification","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Bj\u00f8rner, N., de Moura, L.: $$\\mu $$z\u2013 an efficient engine for fixed points with constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 457\u2013462. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_36"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 265\u2013281. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_19"},{"issue":"2","key":"4_CR29","doi-asserted-by":"publisher","first-page":"161","DOI":"10.3233\/AIC-140640","volume":"28","author":"M Janota","year":"2015","unstructured":"Janota, M., Lynce, I., Marques-Silva, J.: Algorithms for computing backbones of propositional formulae. AI Commun. 28(2), 161\u2013177 (2015). https:\/\/doi.org\/10.3233\/AIC-140640","journal-title":"AI Commun."},{"key":"4_CR30","unstructured":"Janota, M., Marques-Silva, J.: Solving QBF by clause selection. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25\u201331 July 2015, pp. 325\u2013331 (2015). http:\/\/ijcai.org\/Abstract\/15\/052"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-642-22110-1_39","volume-title":"Computer Aided Verification","author":"AK John","year":"2011","unstructured":"John, A.K., Chakraborty, S.: A quantifier elimination algorithm for linear modular equations and disequations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 486\u2013503. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_39"},{"issue":"3","key":"4_CR32","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/s10703-016-0260-9","volume":"49","author":"AK John","year":"2016","unstructured":"John, A.K., Chakraborty, S.: A layered algorithm for quantifier elimination from linear modular constraints. Form. Methods Syst. Des. 49(3), 272\u2013323 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0260-9","journal-title":"Form. Methods Syst. Des."},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-52234-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Jovanovi\u0107","year":"2017","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330\u2013346. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_18"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"4_CR35","unstructured":"Kapur, D., Zarba, C.: A reduction approach to decision procedures. Technical report, University of New Mexico (2006). https:\/\/www.cs.unm.edu\/~kapur\/mypapers\/reduction.pdf"},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2"},{"issue":"2","key":"4_CR37","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/s10601-015-9183-0","volume":"21","author":"MH Liffiton","year":"2016","unstructured":"Liffiton, M.H., Previti, A., Malik, A., Marques-Silva, J.: Fast, flexible mus enumeration. Constraints 21(2), 223\u2013250 (2016)","journal-title":"Constraints"},{"issue":"2","key":"4_CR38","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3166064","volume":"61","author":"NP Lopes","year":"2018","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Practical verification of peephole optimizations with alive. Commun. ACM 61(2), 84\u201391 (2018). https:\/\/doi.org\/10.1145\/3166064","journal-title":"Commun. ACM"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-08867-9_16","volume-title":"Computer Aided Verification","author":"Kenneth L. McMillan","year":"2014","unstructured":"McMillan, K.L.: Lazy annotation revisited. In: Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, 18\u201322 July 2014, Proceedings, pp. 243\u2013259 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_16"},{"key":"4_CR40","unstructured":"Menc\u00eda, C., Previti, A., Marques-Silva, J.: Literal-based MCS extraction. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, 25\u201331 July 2015, pp. 1973\u20131979 (2015). http:\/\/ijcai.org\/Abstract\/15\/280"},{"key":"4_CR41","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-89439-1_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Monniaux","year":"2008","unstructured":"Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 243\u2013257. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89439-1_18"},{"key":"4_CR42","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, 22 November 2008, CEUR Workshop Proceedings, vol. 418. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-418\/paper10.pdf"},{"key":"4_CR43","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15\u201318 November 2009, Austin, Texas, USA, pp. 45\u201352 (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351142","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"4_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_2"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-Matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-642-14203-1_34","volume-title":"Automated Reasoning","author":"L de Moura","year":"2010","unstructured":"de Moura, L., Bj\u00f8rner, N.: Bugs, moles and skeletons: symbolic reasoning for software development. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 400\u2013411. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_34"},{"key":"4_CR48","unstructured":"Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSat resolution. In: Brodley, C.E., Stone, P. (eds.) AAAI 2014, 27\u201331 July 2014, Quebec City, Quebec, Canada, pp. 2717\u20132723. AAAI Press (2014)"},{"key":"4_CR49","doi-asserted-by":"publisher","unstructured":"Narodytska, N., Bj\u00f8rner, N., Marinescu, M., Sagiv, M.: Core-guided minimal correction set and core enumeration. In: Lang, J. (ed.) Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, 13\u201319 July 2018, Stockholm, Sweden, pp. 1353\u20131361. ijcai.org (2018). https:\/\/doi.org\/10.24963\/ijcai.2018\/188","DOI":"10.24963\/ijcai.2018\/188"},{"issue":"2","key":"4_CR50","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979). https:\/\/doi.org\/10.1145\/357073.357079","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"issue":"6","key":"4_CR52","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"4_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-66263-3_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"A Previti","year":"2017","unstructured":"Previti, A., Menc\u00eda, C., J\u00e4rvisalo, M., Marques-Silva, J.: Improving MCS enumeration via caching. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 184\u2013194. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_12"},{"key":"4_CR54","doi-asserted-by":"crossref","unstructured":"Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"4_CR55","unstructured":"Seidl, M., Lonsing, F., Biere, A.: qbf2epr: a tool for generating EPR formulas from QBF. In: Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, 30 June\u20131 July 2012, pp. 139\u2013148 (2012). http:\/\/www.easychair.org\/publications\/paper\/145184"},{"issue":"5","key":"4_CR56","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"4_CR57","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"RE Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975). https:\/\/doi.org\/10.1145\/321879.321884","journal-title":"J. ACM"},{"issue":"2","key":"4_CR58","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/3040488","volume":"64","author":"M Veanes","year":"2017","unstructured":"Veanes, M., Bj\u00f8rner, N., Nachmanson, L., Bereg, S.: Monadic decomposition. J. ACM 64(2), 14:1\u201314:28 (2017). https:\/\/doi.org\/10.1145\/3040488","journal-title":"J. ACM"},{"issue":"1","key":"4_CR59","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10703-012-0156-2","volume":"42","author":"CM Wintersteiger","year":"2013","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.M.: Efficiently solving quantified bit-vector formulas. Form. Methods Syst. Des. 42(1), 3\u201323 (2013)","journal-title":"Form. Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17601-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T04:42:40Z","timestamp":1757306560000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17601-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030176006","9783030176013"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17601-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.swu-rise.net.cn\/SETSS2018\/SETSS2018.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"100% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}