{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,18]],"date-time":"2026-06-18T17:38:16Z","timestamp":1781804296191,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,3]],"date-time":"2018-09-03T00:00:00Z","timestamp":1535932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["647295"],"award-info":[{"award-number":["647295"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L002795\/1"],"award-info":[{"award-number":["EP\/L002795\/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":[[2018,9,3]]},"DOI":"10.1145\/3238147.3238179","type":"proceedings-article","created":{"date-parts":[[2018,8,20]],"date-time":"2018-08-20T20:04:36Z","timestamp":1534795476000},"page":"430-440","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["PARTI: a multi-interval theory solver for symbolic execution"],"prefix":"10.1145","author":[{"given":"Oscar Soria","family":"Dustmann","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Klaus","family":"Wehrle","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,9,3]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"138","volume-title":"Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS","author":"Anand Saswat","year":"2007","unstructured":"Saswat Anand , Corina S. P\u0103s\u0103reanu , and Willem Visser . JPF\u2013SE : A Symbolic Execution Extension to Java PathFinder . In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007 ), pages 134\u2013 138 . Springer Berlin Heidelberg, 2007. Saswat Anand, Corina S. P\u0103s\u0103reanu, and Willem Visser. JPF\u2013SE: A Symbolic Execution Extension to Java PathFinder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), pages 134\u2013138. Springer Berlin Heidelberg, 2007."},{"key":"e_1_3_2_1_2_1","volume-title":"Fr\u00e9d\u00e9ric Goualard. Interval Constraints: Results and Perspectives. In In Proceedings of the Joint ERCIM\/Compulog NetWorkshop on New Trends in Constraints","author":"Benhamou Fr\u00e9d\u00e9ric","year":"1999","unstructured":"Fr\u00e9d\u00e9ric Benhamou , Laurent Granvilliers , and Fr\u00e9d\u00e9ric Goualard. Interval Constraints: Results and Perspectives. In In Proceedings of the Joint ERCIM\/Compulog NetWorkshop on New Trends in Constraints , 1999 . Fr\u00e9d\u00e9ric Benhamou, Laurent Granvilliers, and Fr\u00e9d\u00e9ric Goualard. Interval Constraints: Results and Perspectives. In In Proceedings of the Joint ERCIM\/Compulog NetWorkshop on New Trends in Constraints, 1999."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00142-2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_3_2_1_5_1","first-page":"560","volume-title":"Roberto Sebastiani. A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV","author":"Bruttomesso Roberto","year":"2007","unstructured":"Roberto Bruttomesso , Alessandro Cimatti , Anders Franz\u00e9n , Alberto Griggio , Ziyad Hanna , Alexander Nadel , Amit Palti , and Roberto Sebastiani. A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007 ), pages 547\u2013 560 . Springer Berlin Heidelberg, 2007. Roberto Bruttomesso, Alessandro Cimatti, Anders Franz\u00e9n, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, and Roberto Sebastiani. A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), pages 547\u2013560. Springer Berlin Heidelberg, 2007."},{"key":"e_1_3_2_1_6_1","volume-title":"September 3\u20137","author":"PARTI","year":"2018","unstructured":"PARTI : A Multi-interval Theory Solver for Symbolic Execution ASE \u201918 , September 3\u20137 , 2018 , Montpellier , France PARTI: A Multi-interval Theory Solver for Symbolic Execution ASE \u201918, September 3\u20137, 2018, Montpellier, France"},{"key":"e_1_3_2_1_7_1","first-page":"224","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908) , pages 209\u2013 224 . USENIX Association, 2008. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908), pages 209\u2013224. USENIX Association, 2008."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_10_1","first-page":"149","volume-title":"Future Computing Systems","author":"Cleary J. G.","year":"1987","unstructured":"J. G. Cleary . Logical Arithmetic . Future Computing Systems , pages 125\u2013 149 , 1987 . J. G. Cleary. Logical Arithmetic. Future Computing Systems, pages 125\u2013149, 1987."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_1_14_1","first-page":"1","volume":"2","author":"Dutertre Bruno","year":"2006","unstructured":"Bruno Dutertre and Leonardo De Moura . The YICES SMT Solver. volume 2 , pages 1 \u2013 2 , 2006 . Bruno Dutertre and Leonardo De Moura. The YICES SMT Solver. volume 2, pages 1\u20132, 2006.","journal-title":"The YICES SMT Solver."},{"key":"e_1_3_2_1_15_1","unstructured":"Free Software Foundation. Binutils 2018-07-19.  Free Software Foundation. Binutils 2018-07-19."},{"key":"e_1_3_2_1_16_1","volume-title":"Coreutils - GNU core utilities","author":"Foundation Free Software","year":"2018","unstructured":"Free Software Foundation . Coreutils - GNU core utilities , 2018 -07-19. Free Software Foundation. Coreutils - GNU core utilities, 2018-07-19."},{"key":"e_1_3_2_1_17_1","first-page":"531","volume-title":"Ganesh and David L. Dill. A Decision Procedure for Bit-Vectors and Arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV","author":"Vijay","year":"2007","unstructured":"Vijay Ganesh and David L. Dill. A Decision Procedure for Bit-Vectors and Arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007 ), pages 519\u2013 531 . Springer Berlin Heidelberg, 2007. Vijay Ganesh and David L. Dill. A Decision Procedure for Bit-Vectors and Arrays. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), pages 519\u2013531. Springer Berlin Heidelberg, 2007."},{"key":"e_1_3_2_1_18_1","first-page":"166","volume-title":"David Molnar. Automated Whitebox Fuzz Testing. In Proceedings of the 16th Annual Network and Distributed System Security Symposium (NDSS\u201908)","volume":"8","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Michael Y Levin , and David Molnar. Automated Whitebox Fuzz Testing. In Proceedings of the 16th Annual Network and Distributed System Security Symposium (NDSS\u201908) , volume 8 , pages 151\u2013 166 , 2008 . Patrice Godefroid, Michael Y Levin, and David Molnar. Automated Whitebox Fuzz Testing. In Proceedings of the 16th Annual Network and Distributed System Security Symposium (NDSS\u201908), volume 8, pages 151\u2013166, 2008."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132973.1132980"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_45"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(73)90067-8"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/502102.502106"},{"key":"e_1_3_2_1_24_1","volume-title":"Intel\u00aeXeon\u00aeProcessor E5-2643 v4","author":"Intel Corporation","year":"2018","unstructured":"Intel Corporation . Intel\u00aeXeon\u00aeProcessor E5-2643 v4 , 2018 -07-19. Intel Corporation. Intel\u00aeXeon\u00aeProcessor E5-2643 v4, 2018-07-19."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771806"},{"key":"e_1_3_2_1_26_1","first-page":"615","volume-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911)","author":"Li Guodong","unstructured":"Guodong Li , Indradeep Ghosh , and Sreeranga P. Rajan . KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs . In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911) , pages 609\u2013 615 . Springer Berlin Heidelberg, 2011. Guodong Li, Indradeep Ghosh, and Sreeranga P. Rajan. KLOVER: A Symbolic Execution and Automatic Test Generation Tool for C++ Programs. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV\u201911), pages 609\u2013615. Springer Berlin Heidelberg, 2011."},{"key":"e_1_3_2_1_27_1","first-page":"68","volume-title":"Palikareva and Cristian Cadar. Multi-solver Support in Symbolic Execution. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV","author":"Hristina","year":"2013","unstructured":"Hristina Palikareva and Cristian Cadar. Multi-solver Support in Symbolic Execution. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013 ), pages 53\u2013 68 . Springer Berlin Heidelberg, 2013. Hristina Palikareva and Cristian Cadar. Multi-solver Support in Symbolic Execution. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), pages 53\u201368. Springer Berlin Heidelberg, 2013."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092728"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2016.0046"},{"key":"e_1_3_2_1_30_1","first-page":"36","volume-title":"MBMV","author":"Scheibler Karsten","year":"2014","unstructured":"Karsten Scheibler and Bernd Becker . Implication Graph Compression inside the SMT Solver iSAT3 . In MBMV , pages 25\u2013 36 , 2014 . Karsten Scheibler and Bernd Becker. Implication Graph Compression inside the SMT Solver iSAT3. In MBMV, pages 25\u201336, 2014."},{"key":"e_1_3_2_1_31_1","first-page":"206","volume-title":"Scheibler and Bernd Becker. Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201914)","author":"Karsten","year":"2014","unstructured":"Karsten Scheibler and Bernd Becker. Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201914) , pages 32:203\u201332: 206 , 2014 . Karsten Scheibler and Bernd Becker. Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD\u201914), pages 32:203\u201332:206, 2014."},{"key":"e_1_3_2_1_32_1","volume-title":"OSDI\u201908 Coreutils Experiments","author":"Team KLEE","year":"2018","unstructured":"KLEE Team . OSDI\u201908 Coreutils Experiments , 2018 -07-19. KLEE Team. OSDI\u201908 Coreutils Experiments, 2018-07-19."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0284-9"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393665"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"}],"event":{"name":"ASE '18: 33rd ACM\/IEEE International Conference on Automated Software Engineering","location":"Montpellier France","acronym":"ASE '18","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","CNRS Centre National De La Rechercue Scientifique","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"]},"container-title":["Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3238179","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3238147.3238179","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:39:35Z","timestamp":1750210775000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3238147.3238179"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,3]]},"references-count":35,"alternative-id":["10.1145\/3238147.3238179","10.1145\/3238147"],"URL":"https:\/\/doi.org\/10.1145\/3238147.3238179","relation":{},"subject":[],"published":{"date-parts":[[2018,9,3]]},"assertion":[{"value":"2018-09-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}