{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:36:18Z","timestamp":1770291378980,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":66,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,12]],"date-time":"2019-08-12T00:00:00Z","timestamp":1565568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/N007166\/1,EP\/P010040\/1,EP\/R006865\/1"],"award-info":[{"award-number":["EP\/N007166\/1,EP\/P010040\/1,EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,12]]},"DOI":"10.1145\/3338906.3338921","type":"proceedings-article","created":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T12:21:03Z","timestamp":1565353263000},"page":"521-532","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Just fuzz it: solving floating-point constraints using coverage-guided fuzzing"],"prefix":"10.1145","author":[{"given":"Daniel","family":"Liew","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"J. Ryan","family":"Stinnett","sequence":"additional","affiliation":[{"name":"Mozilla, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,8,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1114284.1114514"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2009.52"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2013.17"},{"key":"e_1_3_2_1_4_1","volume-title":"Sample Survey Principles and Methods (3 ed.)","author":"Barnett Vic","unstructured":"Vic Barnett . 2009. Sample Survey Principles and Methods (3 ed.) . John Wiley & amp; Sons, Chapter 4. Vic Barnett. 2009. Sample Survey Principles and Methods (3 ed.). John Wiley & Sons, Chapter 4."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429133"},{"key":"e_1_3_2_1_6_1","volume-title":"CVC4 at the SMT Competition","author":"Barrett Clark","year":"2018","unstructured":"Clark Barrett , Haniel Barbosa , Martin Brain , Duligur Ibeling , Tim King , Paul Meng , Aina Niemetz , Andres N\u00f6tzli , Mathias Preiner , Andrew Reynolds , and Cesare Tinelli . 2018. CVC4 at the SMT Competition 2018 . CoRR abs\/1806.08775 (2018). arXiv: 1806.08775 Clark Barrett, Haniel Barbosa, Martin Brain, Duligur Ibeling, Tim King, Paul Meng, Aina Niemetz, Andres N\u00f6tzli, Mathias Preiner, Andrew Reynolds, and Cesare Tinelli. 2018. CVC4 at the SMT Competition 2018. CoRR abs\/1806.08775 (2018). arXiv: 1806.08775"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168461"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.91"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1133626.1133628"},{"key":"e_1_3_2_1_13_1","volume-title":"Proc. of the 15th International Workshop on Satisfiability Modulo Theories (SMT\u201917). http:\/\/smt-workshop.cs.uiowa.edu\/2017\/papers\/ SMT2017_paper_21","author":"Marre Bruno","year":"2017","unstructured":"Bruno Marre and Fran\u00c3\u011fois Bobot and Zakaria Chihani . 2017 . Real Behavior of Floating Point Numbers . In Proc. of the 15th International Workshop on Satisfiability Modulo Theories (SMT\u201917). http:\/\/smt-workshop.cs.uiowa.edu\/2017\/papers\/ SMT2017_paper_21 .pdf Bruno Marre and Fran\u00c3\u011fois Bobot and Zakaria Chihani. 2017. Real Behavior of Floating Point Numbers. In Proc. of the 15th International Workshop on Satisfiability Modulo Theories (SMT\u201917). http:\/\/smt-workshop.cs.uiowa.edu\/2017\/papers\/ SMT2017_paper_21.pdf"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908) . Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI\u201908)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009846"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1119772.1119831"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593735.2593737"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966475"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_18"},{"key":"e_1_3_2_1_23_1","volume-title":"Theorem Proving in Higher Order Logics, Richard J","author":"Daumas Marc","unstructured":"Marc Daumas , Laurence Rideau , and Laurent Th\u00e9ry . 2001. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing . In Theorem Proving in Higher Order Logics, Richard J . Boulton and Paul B. Jackson (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 169\u2013184. Marc Daumas, Laurence Rideau, and Laurent Th\u00e9ry. 2001. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. In Theorem Proving in Higher Order Logics, Richard J. Boulton and Paul B. Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 169\u2013184."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_26_1","volume-title":"XSat: A Fast Floating-Point Satisfiability Solver","author":"Fu Zhoulai","unstructured":"Zhoulai Fu and Zhendong Su. 2016. XSat: A Fast Floating-Point Satisfiability Solver . Springer International Publishing , Cham , 187\u2013209. 3-319-41540-6_11 Zhoulai Fu and Zhendong Su. 2016. XSat: A Fast Floating-Point Satisfiability Solver. Springer International Publishing, Cham, 187\u2013209. 3-319-41540-6_11"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062383"},{"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","volume-title":"Proc. of the 15th Network and Distributed System Security Symposium (NDSS\u201908)","author":"Godefroid Patrice","unstructured":"Patrice Godefroid , Michael Y. Levin , and David A. Molnar . 2008. Automated Whitebox Fuzz Testing . In Proc. of the 15th Network and Distributed System Security Symposium (NDSS\u201908) . Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Proc. of the 15th Network and Distributed System Security Symposium (NDSS\u201908)."},{"key":"e_1_3_2_1_30_1","volume-title":"Vienna","author":"Gu Yijia","year":"2015","unstructured":"Yijia Gu , Thomas Wahl , Mahsa Bayati , and Miriam Leeser . 2015 . Behavioral Nonportability in Scientific Numeric Computing. In Euro-Par 2015: Parallel Processing - 21st International Conference on Parallel and Distributed Computing , Vienna , Austria, August 24-28, 2015, Proceedings. 558\u2013569. Yijia Gu, Thomas Wahl, Mahsa Bayati, and Miriam Leeser. 2015. Behavioral Nonportability in Scientific Numeric Computing. In Euro-Par 2015: Parallel Processing - 21st International Conference on Parallel and Distributed Computing, Vienna, Austria, August 24-28, 2015, Proceedings. 558\u2013569."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_1_33_1","volume-title":"Adaptation in natural and artificial systems: an introductory analysis with applications to biology, control, and artificial intelligence","author":"Holland J.H.","unstructured":"J.H. Holland . 1975. Adaptation in natural and artificial systems: an introductory analysis with applications to biology, control, and artificial intelligence . University of Michigan Press. J.H. Holland. 1975. Adaptation in natural and artificial systems: an introductory analysis with applications to biology, control, and artificial intelligence. University of Michigan Press."},{"key":"e_1_3_2_1_34_1","first-page":"4610935","article-title":"2008","volume":"2008","author":"IEEE","year":"2008","unstructured":"IEEE 754- 2008 2008 . IEEE Standard for Floating-Point Arithmetic. Standard. Institute of Electrical and Electronics Engineers. 2008 . 4610935 IEEE 754-2008 2008. IEEE Standard for Floating-Point Arithmetic. Standard. Institute of Electrical and Electronics Engineers. 2008.4610935","journal-title":"IEEE Standard for Floating-Point Arithmetic. Standard. Institute of Electrical and Electronics Engineers."},{"key":"e_1_3_2_1_35_1","volume-title":"ICTSS 2010, Natal, Brazil, November 8-10, 2010. Proceedings, Alexandre Petrenko, Adenilso Sim\u00e3o, and Jos\u00e9 Carlos Maldonado (Eds.). Springer Berlin Heidelberg","author":"Lakhotia Kiran","year":"2010","unstructured":"Kiran Lakhotia , Nikolai Tillmann , Mark Harman , and Jonathan de Halleux . 2010 . FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. In Testing Software and Systems: 22nd IFIP WG 6.1 International Conference , ICTSS 2010, Natal, Brazil, November 8-10, 2010. Proceedings, Alexandre Petrenko, Adenilso Sim\u00e3o, and Jos\u00e9 Carlos Maldonado (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 142\u2013157. Kiran Lakhotia, Nikolai Tillmann, Mark Harman, and Jonathan de Halleux. 2010. FloPSy - Search-Based Floating Point Constraint Solving for Symbolic Execution. In Testing Software and Systems: 22nd IFIP WG 6.1 International Conference, ICTSS 2010, Natal, Brazil, November 8-10, 2010. Proceedings, Alexandre Petrenko, Adenilso Sim\u00e3o, and Jos\u00e9 Carlos Maldonado (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 142\u2013157."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814299"},{"key":"e_1_3_2_1_38_1","unstructured":"2814299  2814299"},{"key":"e_1_3_2_1_39_1","volume-title":"Automation Test in Europe Conference Exhibition (DATE). 1\u20134.","author":"Leeser M.","year":"2014","unstructured":"M. Leeser , S. Mukherjee , J. Ramachandran , and T. Wahl . 2014. Make it real: Effective floating-point reasoning via exact arithmetic. In 2014 Design , Automation Test in Europe Conference Exhibition (DATE). 1\u20134. 2014 .130 M. Leeser, S. Mukherjee, J. Ramachandran, and T. Wahl. 2014. Make it real: Effective floating-point reasoning via exact arithmetic. In 2014 Design, Automation Test in Europe Conference Exhibition (DATE). 1\u20134. 2014.130"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201910)","author":"Leino K. Rustan M.","year":"2009","unstructured":"K. Rustan M. Leino . 2009 . Dafny: An Automatic Program Verifier for Functional Correctness . In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201910) . 348\u2013370. K. Rustan M. Leino. 2009. Dafny: An Automatic Program Verifier for Functional Correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201910). 348\u2013370."},{"key":"e_1_3_2_1_41_1","unstructured":"libfuzzer {n.d.}. LibFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html.  libfuzzer {n.d.}. LibFuzzer. http:\/\/llvm.org\/docs\/LibFuzzer.html."},{"key":"e_1_3_2_1_42_1","unstructured":"libfuzzerbugs {n.d.}. LibFuzzer trophies. http:\/\/llvm.org\/docs\/LibFuzzer.html# trophies.  libfuzzerbugs {n.d.}. LibFuzzer trophies. http:\/\/llvm.org\/docs\/LibFuzzer.html# trophies."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155637"},{"key":"e_1_3_2_1_44_1","volume-title":"Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM","author":"Menendez David","unstructured":"David Menendez , Santosh Nagarakatte , and Aarti Gupta . 2016. Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM . Springer Berlin Heidelberg , Berlin, Heidelberg , 317\u2013337. 978-3-662-53413-7_16 David Menendez, Santosh Nagarakatte, and Aarti Gupta. 2016. Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. Springer Berlin Heidelberg, Berlin, Heidelberg, 317\u2013337. 978-3-662-53413-7_16"},{"key":"e_1_3_2_1_45_1","volume-title":"\u201cbug-o-rama","author":"Zalewski Michal","year":"2019","unstructured":"Michal Zalewski . {n.d.}. AFL \u201cbug-o-rama \u201d trophy case. http:\/\/lcamtuf.coredump. cx\/afl\/#bugs. ESEC\/FSE \u201919, August 26\u201330, 2019 , Tallinn, Estonia D. Liew, C. Cadar, A. F. Donaldson, and J. R. Stinnett Michal Zalewski. {n.d.}. AFL \u201cbug-o-rama\u201d trophy case. http:\/\/lcamtuf.coredump. cx\/afl\/#bugs. ESEC\/FSE \u201919, August 26\u201330, 2019, Tallinn, Estonia D. Liew, C. Cadar, A. F. Donaldson, and J. R. Stinnett"},{"key":"e_1_3_2_1_46_1","unstructured":"Michal Zalewski. {n.d.}. Technical \u201cwhitepaper\u201d for afl-fuzz. http:\/\/lcamtuf. coredump.cx\/afl\/technical_details.txt.  Michal Zalewski. {n.d.}. Technical \u201cwhitepaper\u201d for afl-fuzz. http:\/\/lcamtuf. coredump.cx\/afl\/technical_details.txt."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","unstructured":"C. Michel M. Rueher and Y. Lebbah. 2001. Solving Constraints over Floating-Point Numbers. In Principles and Practice of Constraint Programming \u2014 CP 2001 Toby Walsh (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 524\u2013538.   C. Michel M. Rueher and Y. Lebbah. 2001. Solving Constraints over Floating-Point Numbers. In Principles and Practice of Constraint Programming \u2014 CP 2001 Toby Walsh (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 524\u2013538.","DOI":"10.1007\/3-540-45578-7_36"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931021.2931024"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_3"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_3_2_1_51_1","volume-title":"Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering 20, 3 (01","author":"P\u0103s\u0103reanu Corina S.","year":"2013","unstructured":"Corina S. P\u0103s\u0103reanu , Willem Visser , David Bushnell , Jaco Geldenhuys , Peter Mehlitz , and Neha Rungta . 2013. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering 20, 3 (01 Sept. 2013 ), 391\u2013425. Corina S. P\u0103s\u0103reanu, Willem Visser, David Bushnell, Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta. 2013. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering 20, 3 (01 Sept. 2013), 391\u2013425."},{"key":"e_1_3_2_1_52_1","volume-title":"Automated Test Case Generation with SMT-Solving and Abstract Interpretation","author":"Peleska Jan","unstructured":"Jan Peleska , Elena Vorobev , and Florian Lapschies . 2011. Automated Test Case Generation with SMT-Solving and Abstract Interpretation . In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 298\u2013312. Jan Peleska, Elena Vorobev, and Florian Lapschies. 2011. Automated Test Case Generation with SMT-Solving and Abstract Interpretation. In NASA Formal Methods, Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 298\u2013312."},{"key":"e_1_3_2_1_53_1","volume-title":"Dagstuhl Castle","author":"Putot Sylvie","year":"2003","unstructured":"Sylvie Putot , Eric Goubault , and Matthieu Martel . 2003 . Static Analysis-Based Validation of Floating-Point Computations. In Numerical Software with Result Verification, International Dagstuhl Seminar , Dagstuhl Castle , Germany, January 19-24, 2003, Revised Papers. 306\u2013313. Sylvie Putot, Eric Goubault, and Matthieu Martel. 2003. Static Analysis-Based Validation of Floating-Point Computations. In Numerical Software with Result Verification, International Dagstuhl Seminar, Dagstuhl Castle, Germany, January 19-24, 2003, Revised Papers. 306\u2013313."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2983966"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2693208.2693242"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884850"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503296"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_59_1","unstructured":"SMT-COMP Competition 2006 2006. SMT-COMP Competition 2006. http:\/\/ smtcomp.sourceforge.net\/2006\/.  SMT-COMP Competition 2006 2006. SMT-COMP Competition 2006. http:\/\/ smtcomp.sourceforge.net\/2006\/."},{"key":"e_1_3_2_1_60_1","unstructured":"SMT-LIB. 2018. QF_BV benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMTLIB-benchmarks\/QF_BV.git revision f7e691bf.  SMT-LIB. 2018. QF_BV benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMTLIB-benchmarks\/QF_BV.git revision f7e691bf."},{"key":"e_1_3_2_1_61_1","unstructured":"SMT-LIB. 2018. QF_BV_FP benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/ SMT-LIB-benchmarks\/QF_BVFP.git revision 57d0c730.  SMT-LIB. 2018. QF_BV_FP benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/ SMT-LIB-benchmarks\/QF_BVFP.git revision 57d0c730."},{"key":"e_1_3_2_1_62_1","unstructured":"SMT-LIB. 2018. QF_FP benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMTLIB-benchmarks\/QF_FP.git revision 3346ad7a.  SMT-LIB. 2018. QF_FP benchmarks. https:\/\/clc-gitlab.cs.uiowa.edu:2443\/SMTLIB-benchmarks\/QF_FP.git revision 3346ad7a."},{"key":"e_1_3_2_1_63_1","volume-title":"Proceedings of the Third International Conference on NASA Formal Methods (NFM\u201911)","author":"Souza Matheus","year":"1986","unstructured":"Matheus Souza , Mateus Borges , Marcelo d\u2019 Amorim , and Corina S. P\u0103s\u0103reanu . 2011. CORAL: Solving Complex Constraints for Symbolic Pathfinder . In Proceedings of the Third International Conference on NASA Formal Methods (NFM\u201911) . Springer-Verlag, Berlin, Heidelberg, 359\u2013374. http:\/\/dl.acm.org\/citation.cfm?id= 1986 308. Matheus Souza, Mateus Borges, Marcelo d\u2019Amorim, and Corina S. P\u0103s\u0103reanu. 2011. CORAL: Solving Complex Constraints for Symbolic Pathfinder. In Proceedings of the Third International Conference on NASA Formal Methods (NFM\u201911). Springer-Verlag, Berlin, Heidelberg, 359\u2013374. http:\/\/dl.acm.org\/citation.cfm?id=1986308."},{"key":"e_1_3_2_1_64_1","unstructured":"1986337  1986337"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-010-0124-1"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792798"},{"key":"e_1_3_2_1_67_1","volume-title":"On the complexity of derivation in propositional calculus. Constructive Mathematics and Mathematical Logic","author":"Tseytin G. S.","year":"1970","unstructured":"G. S. Tseytin . 1970. On the complexity of derivation in propositional calculus. Constructive Mathematics and Mathematical Logic ( 1970 ), 115\u2013125. G. S. Tseytin. 1970. On the complexity of derivation in propositional calculus. Constructive Mathematics and Mathematical Logic (1970), 115\u2013125."}],"event":{"name":"ESEC\/FSE '19: 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Tallinn Estonia","acronym":"ESEC\/FSE '19","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338906.3338921","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3338906.3338921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:20Z","timestamp":1750206380000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3338906.3338921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,12]]},"references-count":66,"alternative-id":["10.1145\/3338906.3338921","10.1145\/3338906"],"URL":"https:\/\/doi.org\/10.1145\/3338906.3338921","relation":{},"subject":[],"published":{"date-parts":[[2019,8,12]]},"assertion":[{"value":"2019-08-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}