{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:17:37Z","timestamp":1742930257152,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031505232"},{"type":"electronic","value":"9783031505249"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-50524-9_12","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T15:02:28Z","timestamp":1703862148000},"page":"258-279","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Function Synthesis for\u00a0Maximizing Model Counting"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6396-0285","authenticated-orcid":false,"given":"Thomas","family":"Vigouroux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4412-5684","authenticated-orcid":false,"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6322-0383","authenticated-orcid":false,"given":"Cristian","family":"Ene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9925-098X","authenticated-orcid":false,"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"12_CR1","unstructured":"Audemard, G., Lagniez, J., Miceli, M.: A new exact solver for (weighted) max#SAT. In: SAT. LIPIcs, vol. 236, pp. 28:1\u201328:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Aziz, R.A., Chu, G., Muise, C., Stuckey, P.: $$\\#\\exists $$SAT: projected model counting. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 121\u2013137. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_10","DOI":"10.1007\/978-3-319-24318-4_10"},{"key":"12_CR3","unstructured":"Bardin, S., Girol, G.: A Quantitative Flavour of Robust Reachability. arXiv preprint arXiv:2212.05244 (2022)"},{"key":"12_CR4","unstructured":"Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: IJCAI, pp. 689\u2013695. AAAI Press (2015)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: A Scalable Approximate Model Counter. arXiv preprint arXiv:1306.5726 (2013)","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing Scalability and Uniformity in SAT Witness Generator. In: DAC, pp. 60:1\u201360:6. ACM (2014)","DOI":"10.1145\/2593069.2593097"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Chen, P., Huang, Y., Jiang, J.R.: A sharp leap from quantified boolean formula to stochastic boolean satisfiability solving. In: AAAI, pp. 3697\u20133706. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i5.16486"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Cheng, C., Jiang, J.R.: Lifting (D)QBF preprocessing and solving techniques to (D)SSAT. In: AAAI, pp. 3906\u20133914. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i4.25504"},{"issue":"2","key":"12_CR9","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1109\/TETC.2017.2785299","volume":"8","author":"T Dullien","year":"2020","unstructured":"Dullien, T.: Weird machines, exploitability, and provable unexploitability. IEEE Trans. Emerg. Top. Comput. 8(2), 391\u2013403 (2020)","journal-title":"IEEE Trans. Emerg. Top. Comput."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Rabe, M.N., Seshia, S.A.: Maximum model counting. In: AAAI, pp. 3885\u20133892. AAAI Press (2017)","DOI":"10.1609\/aaai.v31i1.11138"},{"key":"12_CR11","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman (1979)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Garey, M.R., Johnson, D.S., So, H.C.: An application of graph coloring to printed circuit testing (working paper). In: FOCS, pp. 178\u2013183 (1975)","DOI":"10.1109\/SFCS.1975.3"},{"key":"12_CR13","unstructured":"Gario, M., Micheli, A.: PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In: SMT Workshop, vol. 2015 (2015)"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"96","DOI":"10.2307\/2270594","volume":"30","author":"L Henkin","year":"1965","unstructured":"Henkin, L., Karp, C.R.: Some remarks on infinitely long formulas. J. Symb. Log. 30(1), 96\u201397 (1965). https:\/\/doi.org\/10.2307\/2270594","journal-title":"J. Symb. Log."},{"issue":"7","key":"12_CR15","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"12_CR16","unstructured":"Kov\u00e1sznai, G.: What is the state-of-the-art in DQBF solving. In: MaCS-16. Joint Conference on Mathematics and Computer Science (2016)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Kullmann, O.: Fundaments of branching heuristics. In: Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 351\u2013390. IOS Press (2021)","DOI":"10.3233\/FAIA200991"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Lagniez, J., Marquis, P.: A recursive algorithm for projected model counting. In: AAAI, pp. 1536\u20131543. AAAI Press (2019)","DOI":"10.1609\/aaai.v33i01.33011536"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Lee, N., Jiang, J.R.: Dependency stochastic boolean satisfiability: a logical formalism for NEXPTIME decision problems with uncertainty. In: AAAI, pp. 3877\u20133885. AAAI Press (2021)","DOI":"10.1609\/aaai.v35i5.16506"},{"issue":"3","key":"12_CR20","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/s10817-023-09670-6","volume":"67","author":"Y Luo","year":"2023","unstructured":"Luo, Y., Cheng, C., Jiang, J.R.: A resolution proof system for dependency stochastic boolean satisfiability. J. Autom. Reason. 67(3), 26 (2023)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"12_CR21","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1016\/0022-0000(85)90045-5","volume":"31","author":"CH Papadimitriou","year":"1985","unstructured":"Papadimitriou, C.H.: Games against nature. J. Comput. Syst. Sci. 31(2), 288\u2013301 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"7\u20138","key":"12_CR22","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","volume":"41","author":"G Peterson","year":"2001","unstructured":"Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Comput. Math. Appl. 41(7\u20138), 957\u2013992 (2001)","journal-title":"Comput. Math. Appl."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Peterson, G.L., Reif, J.H.: Multiple-person alternation. In: FOCS, pp. 348\u2013363. IEEE Computer Society (1979)","DOI":"10.1109\/SFCS.1979.25"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Phan, Q., Bang, L., Pasareanu, C.S., Malacaria, P., Bultan, T.: Synthesis of adaptive side-channel attacks. In: IACR Cryptol. ePrint Arch, p. 401 (2017)","DOI":"10.1109\/CSF.2017.8"},{"key":"12_CR25","unstructured":"Saha, S., Eiers, W., Kadron, I.B., Bang, L., Bultan, T.: Incremental adaptive attack synthesis. arXiv preprint arXiv:1905.05322 (2019)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 288\u2013302. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_21","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"12_CR27","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8405351","author":"T Vigouroux","year":"2023","unstructured":"Vigouroux, T., Bozga, M., Ene, C., Mounier, L.: DQMaxMC Solver (2023). https:\/\/doi.org\/10.5281\/zenodo.8405351","journal-title":"DQMaxMC Solver"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Vigouroux, T., Bozga, M., Ene, C., Mounier, L.: Function synthesis for maximizing model counting. arXiv preprint arXiv:2305.10003 (2023)","DOI":"10.1007\/978-3-031-50524-9_12"},{"key":"12_CR29","unstructured":"Vigouroux, T., Ene, C., Monniaux, D., Mounier, L., Potet, M.: BaxMC: a CEGAR approach to Max#SAT. In: FMCAD, pp. 170\u2013178. IEEE (2022)"},{"key":"12_CR30","unstructured":"Wang, H., Tu, K., Jiang, J.R., Scholl, C.: Quantifier elimination in stochastic boolean satisfiability. In: SAT. LIPIcs, vol. 236, pp. 23:1\u201323:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 473\u2013489. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_29","DOI":"10.1007\/978-3-319-40970-2_29"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50524-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:12:21Z","timestamp":1704240741000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50524-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505232","9783031505249"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50524-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","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":"74","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":"30","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":"41% - 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":"3","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":"6","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)"}}]}}