乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T02:59:39Z","timestamp":1720493979026},"reference-count":186,"publisher":"Elsevier","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.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1016\/bs.adcom.2018.10.002","type":"book-chapter","created":{"date-parts":[[2018,12,21]],"date-time":"2018-12-21T14:04:35Z","timestamp":1545401075000},"page":"225-287","source":"Crossref","is-referenced-by-count":10,"title":["Advances in Symbolic Execution"],"prefix":"10.1016","author":[{"given":"Guowei","family":"Yang","sequence":"first","affiliation":[]},{"given":"Antonio","family":"Filieri","sequence":"additional","affiliation":[]},{"given":"Mateus","family":"Borges","sequence":"additional","affiliation":[]},{"given":"Donato","family":"Clun","sequence":"additional","affiliation":[]},{"given":"Junye","family":"Wen","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"7","key":"10.1016\/bs.adcom.2018.10.002_bb0010","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King","year":"1976","journal-title":"Commun. ACM"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0015","first-page":"488","article-title":"A program testing system","author":"Clarke","year":"1976"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0020","series-title":"Decision Procedures: An Algorithmic Point of View","isbn-type":"print","author":"Kroening","year":"2008","ISBN":"http:\/\/id.crossref.org\/isbn\/9783540741046"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0025","isbn-type":"print","first-page":"213","article-title":"DART: directed automated random testing","author":"Godefroid","year":"2005","ISBN":"http:\/\/id.crossref.org\/isbn\/1595930566"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0030","isbn-type":"print","first-page":"263","article-title":"CUTE: a concolic unit testing engine for C","author":"Sen","year":"2005","ISBN":"http:\/\/id.crossref.org\/isbn\/1595930140"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0035","first-page":"209","article-title":"KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs","author":"Cadar","year":"2008"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0040","isbn-type":"print","first-page":"134","article-title":"Pex: white box test generation for .NET","author":"Tillmann","year":"2008","ISBN":"http:\/\/id.crossref.org\/isbn\/9783540791232"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0045","series-title":"Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications","isbn-type":"print","author":"Biere","year":"2009","ISBN":"http:\/\/id.crossref.org\/isbn\/9781586039295"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0050","isbn-type":"print","first-page":"1","article-title":"Green: reducing, reusing and recycling Constraints in Program Analysis","author":"Visser","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450316149"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0055","isbn-type":"print","first-page":"177","article-title":"Enhancing reuse of constraint solutions to improve symbolic execution","author":"Jia","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336208"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0060","isbn-type":"print","first-page":"305","article-title":"Reusing constraint proofs in program analysis","author":"Aquino","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336208"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0065","series-title":"Lecture Notes in Computer Science (LNCS) (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-3-642-39176-7_19","article-title":"Expression reduction from programs in a symbolic binary executor","volume":"vol. 7976","author":"Romano","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642391750","ISSN":"http:\/\/id.crossref.org\/issn\/0302-9743","issn-type":"print"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0070","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2693208.2693244","article-title":"Minimizing the size of path conditions using convex polyhedra abstract domain","volume":"40","author":"Lloyd","year":"2015","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0075","series-title":"Speculative symbolic execution","isbn-type":"print","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1109\/ISSRE.2012.8","author":"Zhang","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769548883","ISSN":"http:\/\/id.crossref.org\/issn\/1071-9458","issn-type":"print"},{"issue":"6","key":"10.1016\/bs.adcom.2018.10.002_bb0080","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382756.2382792","article-title":"S2PF speculative symbolic pathFinder","volume":"37","author":"Zhang","year":"2012","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0085","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2557833.2560578","article-title":"User-defined backtracking criteria for symbolic execution","volume":"39","author":"Kausler","year":"2014","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0090","series-title":"Tools and Algorithms for the Construction and Analysis of Systems: 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22\u201329, 2009. Proceedings","isbn-type":"print","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","article-title":"Path feasibility analysis for string-manipulating programs","author":"Bj\u00f8rner","year":"2009","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642007682"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0095","first-page":"1","article-title":"Precise analysis of string expressions","volume":"vol. 2694","author":"Christensen","year":"2003"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0100","isbn-type":"print","first-page":"105","article-title":"HAMPI: a solver for string constraints","author":"Kiezun","year":"2009","ISBN":"http:\/\/id.crossref.org\/isbn\/9781605583389"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0105","isbn-type":"print","first-page":"259","article-title":"Evaluation of string constraint solvers in the context of symbolic execution","author":"Kausler","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330138"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0110","isbn-type":"print","first-page":"114","article-title":"Z3-str: a Z3-based string solver for web application analysis","author":"Zheng","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450322379"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0115","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1007\/978-3-319-41528-4_12","article-title":"Progressive reasoning over recursivelydefined strings","volume":"vol. 9779","author":"Trinh","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415277","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0120","isbn-type":"print","first-page":"1232","article-title":"S3: a symbolic string solver for vulnerability detection in web applications","author":"Trinh","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450329576"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0125","isbn-type":"print","first-page":"646","article-title":"A DPLL(T) theory solver for a theory of strings and regular expressions","volume":"vol. 8559","author":"Liang","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319088662"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0130","isbn-type":"print","first-page":"150","article-title":"String constraints for verification","volume":"vol. 8559","author":"Abdulla","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319088662"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0135","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"462","DOI":"10.1007\/978-3-319-21690-4_29","article-title":"Norn: an SMT solver for string constraints","volume":"vol. 9206","author":"Abdulla","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319216898","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0140","series-title":"Symbolic execution with interval solving and meta-heuristic search","isbn-type":"print","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/ICST.2012.91","volume":"vol. 1","author":"Borges","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769546704","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0145","isbn-type":"print","first-page":"425","article-title":"Solving complex path conditions through heuristic search on induced polytopes","author":"Dinges","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330565"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0150","series-title":"Symbolic path-oriented test data generation for floating-point programs","isbn-type":"print","first-page":"1","author":"Bagnara","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769549682","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0155","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-319-41540-6_11","article-title":"Xsat: a fast floating-point satisfiability solver","volume":"vol. 9780","author":"Fu","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415390","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0160","isbn-type":"print","first-page":"554","article-title":"Symbolic execution of complex program driven by machine learning based constraint solving","author":"Li","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450338455"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0165","series-title":"A Nonlinear Real Arithmetic Fragment","first-page":"729","author":"Tiwari","year":"2014"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0170","series-title":"Lecture Notes in Computer Science (LNCS) (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"680","DOI":"10.1007\/978-3-319-08867-9_45","article-title":"A tale of two solvers: eager and lazy approaches to bit-vectors","volume":"vol. 8559","author":"Hadarean","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319088662","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0175","isbn-type":"print","first-page":"55","article-title":"Separation logic: a logic for shared mutable data structures","author":"Reynolds","year":"2002","ISBN":"http:\/\/id.crossref.org\/isbn\/0769514839"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0180","series-title":"Lecture Notes in Computer Science (LNCS) (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","article-title":"Automating separation logic using SMT","volume":"vol. 8044","author":"Piskac","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642397981","ISSN":"http:\/\/id.crossref.org\/issn\/0302-9743","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0185","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-319-41540-6_13","article-title":"Array folds logic","volume":"vol. 9780","author":"Daca","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415390","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0190","first-page":"87","article-title":"Deciding local theory extensions via e-matching","author":"Bansal","year":"2015"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0195","series-title":"A decision procedure for sets, binary relations and partial functions","isbn-type":"print","first-page":"179","volume":"vol. 1","author":"Cristi\u00e1","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319576329","ISSN":"http:\/\/id.crossref.org\/issn\/1865-1348","issn-type":"print"},{"issue":"10","key":"10.1016\/bs.adcom.2018.10.002_bb0200","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2544173.2509553","article-title":"Steering symbolic execution to less traveled paths","volume":"48","author":"Li","year":"2013","journal-title":"ACM SIGPLAN Notices","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0205","isbn-type":"print","first-page":"413","article-title":"How we get there: a context-guided search strategy in concolic testing","author":"Seo","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330565"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0210","series-title":"Guiding dynamic symbolic execution toward unverified program executions","isbn-type":"print","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1145\/2884781.2884843","author":"Christakis","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450339001","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0215","isbn-type":"print","first-page":"276","article-title":"Measuring enforcement windows with symbolic trace interpretation: what well-behaved programs say","author":"Coughlin","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450314541"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0220","series-title":"Regular property guided dynamic symbolic execution","isbn-type":"print","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1109\/ICSE.2015.80","volume":"vol. 1","author":"Zhang","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479919345","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0225","series-title":"Property differencing for incremental checking","isbn-type":"print","doi-asserted-by":"crossref","first-page":"1059","DOI":"10.1145\/2568225.2568319","author":"Yang","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327565","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0230","doi-asserted-by":"crossref","first-page":"3:1","DOI":"10.1145\/2629536","article-title":"Directed incremental symbolic execution","volume":"24","author":"Yang","year":"2014","journal-title":"ACM Trans. Softw. Eng. Methodol.","ISSN":"http:\/\/id.crossref.org\/issn\/1049-331X","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0235","series-title":"Directed incremental symbolic execution","isbn-type":"print","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/1993498.1993558","author":"Person","year":"2011","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450306638","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0240","series-title":"Lecture Notes in Computer Science (LNCS) (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-642-39176-7_7","article-title":"Regression verification using impact summaries","volume":"vol. 7976","author":"Backes","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642391750","ISSN":"http:\/\/id.crossref.org\/issn\/0302-9743","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0245","isbn-type":"print","first-page":"271","article-title":"Incremental symbolic execution for automated test suite maintenance","author":"Makhdoom","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330138"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0250","series-title":"Postconditioned symbolic execution","isbn-type":"print","author":"Yi","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479971251","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"issue":"4","key":"10.1016\/bs.adcom.2018.10.002_bb0255","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2652484","article-title":"Scaling up symbolic analysis by removing Z-equivalent states","volume":"23","author":"Li","year":"2014","journal-title":"Tsem14","ISSN":"http:\/\/id.crossref.org\/issn\/1049-331X","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0260","isbn-type":"print","first-page":"144","article-title":"Memoized symbolic execution","author":"Yang","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450314541"},{"issue":"6","key":"10.1016\/bs.adcom.2018.10.002_bb0265","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/2345156.2254088","article-title":"Efficient state merging in symbolic execution","volume":"47","author":"Kuznetsov","year":"2012","journal-title":"ACM SIGPLAN Notices","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0270","series-title":"A General Lattice Model for Merging Symbolic Execution Branches","isbn-type":"print","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/978-3-319-47846-3_5","volume":"vol. 10009","author":"Scheurer","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319478456"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0275","isbn-type":"print","first-page":"53","article-title":"Boosting concolic testing via interpolation","author":"Jaffar","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450322379"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0280","isbn-type":"print","first-page":"842","article-title":"MultiSE: multi-path symbolic execution using value summaries","author":"Sen","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336758"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0285","isbn-type":"print","first-page":"1083","article-title":"Enhancing symbolic execution with veritesting","author":"Avgerinos","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327565"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0290","isbn-type":"print","first-page":"155","article-title":"Abstracting path conditions","author":"Strej\u010dek","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450314541"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0295","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2693208.2693243","article-title":"Improving coverage of test cases generated by symbolic pathfinder for programs with loops","volume":"40","author":"Kersten","year":"2015","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0300","isbn-type":"print","first-page":"188","article-title":"S-looper: automatic summarization for multipath string loops","author":"Xie","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336208"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0305","series-title":"Segmented symbolic analysis","isbn-type":"print","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1109\/ICSE.2013.6606567","author":"Le","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467330763","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0310","series-title":"Scaling symbolic execution using ranged analysis","isbn-type":"print","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1145\/2384616.2384654","author":"Siddiqui","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450315616","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0315","series-title":"Scaling and Certifying Symbolic Execution (PhD dissertation)","author":"Qiu","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0320","first-page":"130","article-title":"A synergistic approach for distributed symbolic execution using test ranges","author":"Qiu","year":"2017"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0325","series-title":"Industrial application of concolic testing approach: a case study on libexif by using CREST-BV and KLEE","isbn-type":"print","doi-asserted-by":"crossref","first-page":"1143","DOI":"10.1109\/ICSE.2012.6227105","author":"Kim","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467310673","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0330","isbn-type":"print","first-page":"138","article-title":"Looking closer at compositional symbolic execution","author":"Lin","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450337960"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0335","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1145\/1190215.1190226","article-title":"Compositional dynamic test generation","volume":"42","author":"Godefroid","year":"2007","journal-title":"SIGPLAN Not.","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0340","isbn-type":"print","first-page":"213","article-title":"DART: directed automated random testing","author":"Godefroid","year":"2005","ISBN":"http:\/\/id.crossref.org\/isbn\/1595930566"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0345","first-page":"367","article-title":"Demand-driven compositional symbolic execution","author":"Anand","year":"2008"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0350","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1707801.1706307","article-title":"Compositional may-must program analysis: unleashing the power of alternation","volume":"45","author":"Godefroid","year":"2010","journal-title":"SIGPLAN Not.","ISSN":"http:\/\/id.crossref.org\/issn\/0362-1340","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0355","article-title":"Compositional Symbolic Execution Through Program Specialization","author":"Rojas","year":"2013"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0360","series-title":"Partial Evaluation and Automatic Program Generation","isbn-type":"print","author":"Jones","year":"1993","ISBN":"http:\/\/id.crossref.org\/isbn\/0130202495"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0365","isbn-type":"print","first-page":"632","article-title":"Compositional symbolic execution with memoized replay","author":"Qiu","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479919345"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0370","isbn-type":"print","first-page":"213","article-title":"Compositional symbolic execution using fine-grained summaries","author":"Lin","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467393904"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0375","first-page":"780","article-title":"MACKE: compositional analysis of low-level vulnerabilities with symbolic execution","author":"Ognawala","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0380","isbn-type":"print","first-page":"757","article-title":"Using program analysis to synthesize sensor spoofing attacks","author":"Pustogarov","year":"2017","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450349444"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0385","isbn-type":"print","first-page":"382","article-title":"Satisfiability modulo heap-based programs","volume":"vol. 9779","author":"Le","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415277"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0390","isbn-type":"print","first-page":"405","article-title":"Automatic verification of iterated separating conjunctions using symbolic execution","volume":"vol. 9779","author":"M\u00fcller","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415277"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0395","series-title":"NASA Formal Methods: 5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14\u201316, 2013. Proceedings","isbn-type":"print","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-642-38088-4_16","article-title":"Bounded lazy initialization","author":"Geldenhuys","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642380884"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0400","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2557833.2560571","article-title":"Symbolic pathFinder v7","volume":"39","author":"Luckow","year":"2014","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"issue":"7","key":"10.1016\/bs.adcom.2018.10.002_bb0405","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1109\/TSE.2015.2389225","article-title":"BLISS: improved symbolic execution by bounded lazy initialization with SAT support","volume":"41","author":"Rosner","year":"2015","journal-title":"IEEE Trans. Softw. Eng.","ISSN":"http:\/\/id.crossref.org\/issn\/0098-5589","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0410","first-page":"295","article-title":"Efficient symbolic execution of value-based data structures for critical systems","author":"Belt","year":"2012"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0415","series-title":"SPARK\u2014an annotated Ada subset for safety-critical programming","first-page":"392","author":"Carre","year":"1990"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0420","series-title":"Tools and Algorithms for the Construction and Analysis of Systems: 9th International Conference, TACAS 2003 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003 Warsaw, Poland, April 7\u201311, 2003 Proceedings","isbn-type":"print","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-36577-X_40","article-title":"Generalized symbolic execution for model checking and testing","author":"Khurshid","year":"2003","ISBN":"http:\/\/id.crossref.org\/isbn\/9783540365778"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0425","isbn-type":"print","first-page":"411","article-title":"Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization","author":"Braione","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450322379"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0430","isbn-type":"print","first-page":"602","article-title":"Symbolic execution of programs with heap inputs","author":"Braione","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336758"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0435","isbn-type":"print","first-page":"1018","article-title":"JBSE: a symbolic executor for Java programs with complex heap inputs","author":"Braione","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450342186"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0440","isbn-type":"print","first-page":"247","article-title":"symMMU: symbolically executed runtime libraries for symbolic memory access","author":"Romano","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330138"},{"issue":"6","key":"10.1016\/bs.adcom.2018.10.002_bb0445","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3011286.3011296","article-title":"Symbolic arrays in symbolic pathFinder","volume":"41","author":"Fromherz","year":"2016","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0450","isbn-type":"print","first-page":"275","article-title":"Thresher: precise refutations for heap reachability","author":"Blackshear","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450320146"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0455","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-21668-3_1","article-title":"Poling: SMT aided linearizability proofs","volume":"vol. 9207","author":"Zhu","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319216676","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0460","isbn-type":"print","first-page":"399","article-title":"Dangling references in multi-configuration and dynamic PHP-based Web applications","author":"Nguyen","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479902156"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0465","isbn-type":"print","first-page":"387","article-title":"Sound Predictive Race Detection in Polynomial Time","author":"Smaragdakis","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450310833"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0470","isbn-type":"print","first-page":"256","article-title":"Symbolic predictive analysis for concurrent programs","author":"Wang","year":"2009","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642050886"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0475","isbn-type":"print","first-page":"313","article-title":"Generating data race witnesses by an SMT-based analysis","author":"Said","year":"2011","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642203978"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0480","isbn-type":"print","first-page":"59","article-title":"IPA: improving predictive analysis with pointer analysis","author":"Liu","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450343909"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0485","first-page":"239","article-title":"Concurrent test generation using concolic multi-trace analysis","author":"Razavi","year":"2012"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0490","isbn-type":"print","first-page":"443","article-title":"Heuristics for scalable dynamic test generation","author":"Burnim","year":"2008","ISBN":"http:\/\/id.crossref.org\/isbn\/9781424421879"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0495","isbn-type":"print","first-page":"37","article-title":"Con2Colic testing","author":"Farzan","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450322379"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0500","isbn-type":"print","first-page":"166","article-title":"Fast and precise symbolic analysis of concurrency bugs in device drivers (T)","author":"Deligiannis","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781509000258"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0505","isbn-type":"print","first-page":"177","article-title":"ParCoSS: Efficient Parallelized Compiled Symbolic Simulation","author":"Herdt","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319415406"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0510","isbn-type":"print","first-page":"215","article-title":"GKLEE: concolic verification and test generation for GPUs","author":"Li","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450311601"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0515","isbn-type":"print","first-page":"167","article-title":"A randomized scheduler with probabilistic guarantees of finding bugs","author":"Burckhardt","year":"2010","ISBN":"http:\/\/id.crossref.org\/isbn\/9781605588391"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0520","isbn-type":"print","first-page":"446","article-title":"Iterative context bounding for systematic testing of multithreaded programs","author":"Musuvathi","year":"2007","ISBN":"http:\/\/id.crossref.org\/isbn\/9781595936332"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0525","isbn-type":"print","first-page":"150","article-title":"Using unfoldings in automated testing of multithreaded programs","author":"K\u00e4hk\u00f6nen","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450312042"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0530","isbn-type":"print","first-page":"164","article-title":"Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits","author":"McMillan","year":"1993","ISBN":"http:\/\/id.crossref.org\/isbn\/3540564969"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0535","isbn-type":"print","first-page":"854","article-title":"Assertion guided symbolic execution of multithreaded programs","author":"Guo","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336758"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0540","isbn-type":"print","first-page":"531","article-title":"Conc-iSE: incremental symbolic execution of concurrent software","author":"Guo","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450338455"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0545","isbn-type":"print","first-page":"677","article-title":"Input-covering schedules for multithreaded programs","author":"Bergan","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450323741"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0550","isbn-type":"print","first-page":"491","article-title":"Symbolic execution of multithreaded programs from arbitrary program contexts","author":"Bergan","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450325851"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0555","isbn-type":"print","first-page":"915","article-title":"Combining static analysis and constraint solving for automatic test case generation","author":"Vorobyov","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769546704"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0560","isbn-type":"print","first-page":"815","article-title":"Randoop: feedback-directed random testing for Java","author":"Pacheco","year":"2007","ISBN":"http:\/\/id.crossref.org\/isbn\/9781595938657"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0565","series-title":"Feedbackdirected unit test generation for C\/C++ using concolic execution","isbn-type":"print","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1109\/ICSE.2013.6606559","author":"Garg","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467330763","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0570","series-title":"Efficient leveraging of symbolic execution to advanced coverage criteria","isbn-type":"print","first-page":"173","volume":"vol. 7","author":"Bardin","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769551852","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0575","isbn-type":"print","first-page":"228","article-title":"Efficient observability-based test generation by dynamic symbolic execution","author":"You","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781509004065"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0580","series-title":"Observable modified condition\/decision coverage","first-page":"102","author":"Whalen","year":"2013","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0585","isbn-type":"print","first-page":"254","article-title":"Augmented dynamic symbolic execution","author":"Jamrozik","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450312042"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0590","series-title":"Path exploration based on symbolic output","isbn-type":"print","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1145\/2025113.2025152","volume":"vol. 22","author":"Qi","year":"2011","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450304436","ISSN":"http:\/\/id.crossref.org\/issn\/1049-331X","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0595","series-title":"Make test-zesti: a symbolic execution solution for improving regression testing","isbn-type":"print","doi-asserted-by":"crossref","first-page":"716","DOI":"10.1109\/ICSE.2012.6227146","author":"Dan Marinescu","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467310673","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0600","series-title":"ICSE","isbn-type":"print","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1145\/2591062.2591104","article-title":"Shadow symbolic execution for better testing of evolving software","author":"Cadar","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327688","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0605","series-title":"Patch verification via multiversion interprocedural control flow graphs","isbn-type":"print","doi-asserted-by":"crossref","first-page":"1047","DOI":"10.1145\/2568225.2568304","author":"Le","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327565","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0610","isbn-type":"print","first-page":"106","article-title":"FSX: fine-grained incremental unit test generation for C\/C++ programs","author":"Yoshida","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450343909"},{"issue":"3","key":"10.1016\/bs.adcom.2018.10.002_bb0615","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","article-title":"Symbolic Boolean manipulation with ordered binary-decision diagrams","volume":"24","author":"Bryant","year":"1992","journal-title":"ACM Comput. Surv.","ISSN":"http:\/\/id.crossref.org\/issn\/0360-0300","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0620","series-title":"Combining symbolic execution and model checking for data flow testing","isbn-type":"print","doi-asserted-by":"crossref","first-page":"654","DOI":"10.1109\/ICSE.2015.81","volume":"vol. 1","author":"Su","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479919345","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0625","isbn-type":"print","first-page":"89","article-title":"Compositional load test generation for software pipelines","author":"Zhang","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450314541"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0630","isbn-type":"print","first-page":"449","article-title":"SymJS: automatic symbolic testing of JavaScript web applications","author":"Li","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330565"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0635","isbn-type":"print","first-page":"168","article-title":"Type-aware concolic testing of JavaScript programs","author":"Dhok","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450339001"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0640","isbn-type":"print","first-page":"196","article-title":"ExpoSE: practical symbolic execution of standalone javascript","author":"Loring","year":"2017","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450350778"},{"issue":"6","key":"10.1016\/bs.adcom.2018.10.002_bb0645","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2382756.2382798","article-title":"Testing android apps through symbolic execution","volume":"37","author":"Mirzaei","year":"2012","journal-title":"ACM SIGSOFT Softw. Eng. Notes","ISSN":"http:\/\/id.crossref.org\/issn\/0163-5948","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0650","isbn-type":"print","first-page":"461","article-title":"SIG-Droid: automated system input generation for android applications","author":"Mirzaei","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781509004065"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0655","isbn-type":"print","first-page":"1","article-title":"Automated concolic testing of smartphone apps","author":"Anand","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450316149"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0660","isbn-type":"print","first-page":"67","article-title":"Automated testing with targeted event sequence generation","author":"Jensen","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450321594"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0665","isbn-type":"print","first-page":"519","article-title":"Symbolic execution of stored procedures in database management systems","author":"Mahmood","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450338455"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0670","series-title":"Generating succinct test cases using don\u2019t care analysis","isbn-type":"print","author":"Nguyen","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479971251","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0675","series-title":"Using fuzzy logic and symbolic execution to prioritize UML-RT test cases","isbn-type":"print","first-page":"1","author":"Rapos","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479971251","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0680","series-title":"DASE: documentassisted symbolic execution for improving automated software testing","isbn-type":"print","doi-asserted-by":"crossref","first-page":"620","DOI":"10.1109\/ICSE.2015.78","volume":"vol. 1","author":"Wong","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781479919345","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0685","isbn-type":"print","first-page":"49","article-title":"Dowser: a guided fuzzer to find buffer overflow vulnerabilities","author":"Haller","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971034"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0690","first-page":"28","article-title":"AddressSanitizer: a fast address sanity checker","author":"Serebryany","year":"2012"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0695","isbn-type":"print","first-page":"21","article-title":"Driller: augmenting fuzzing through selective symbolic execution","author":"Stephens","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/189156241X"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0700","series-title":"Lazart: a symbolic approach for evaluation the robustness of secured codes against control flow injections","isbn-type":"print","first-page":"213","author":"Potet","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9780769551852","ISSN":"http:\/\/id.crossref.org\/issn\/2159-4848","issn-type":"print"},{"issue":"10","key":"10.1016\/bs.adcom.2018.10.002_bb0705","doi-asserted-by":"crossref","first-page":"1379","DOI":"10.1016\/j.infsof.2009.04.016","article-title":"Higher Order Mutation Testing","volume":"51","author":"Jia","year":"2009","journal-title":"Inf. Softw. Technol.","ISSN":"http:\/\/id.crossref.org\/issn\/0950-5849","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0710","isbn-type":"print","first-page":"463","article-title":"FIE on firmware: finding vulnerabilities in embedded systems using symbolic execution finding vulnerabilities in embedded systems using symbolic execution","author":"Davidson","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971034"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0715","isbn-type":"print","first-page":"49","article-title":"Under-constrained symbolic execution: correctness checking for real code","author":"Ramos","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971232"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0720","isbn-type":"print","first-page":"345","article-title":"Automatically detecting error handling bugs using error specifications","author":"Jana","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971324"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0725","isbn-type":"print","first-page":"363","article-title":"APISan: sanitizing API usages through semantic cross-checking","author":"Yun","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971324"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0730","isbn-type":"print","article-title":"MetaSymploit: day-one defense against script-based attacks with security-enhanced symbolic analysis","author":"Wang","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781931971034"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0735","first-page":"503","article-title":"SymCerts: Practical Symbolic Execution for Exposing Noncompliance in X.509 Certificate Validation Implementations","author":"Chau","year":"2017"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0740","first-page":"387","article-title":"Multi-run side-channel analysis using symbolic execution and Max-SMT","author":"P\u0103s\u0103reanu","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0745","series-title":"Cryptographic Function Detection in Obfuscated Binaries via Bit-Precise Symbolic Loop Mapping","isbn-type":"print","first-page":"921","author":"Xu","year":"2017","ISBN":"http:\/\/id.crossref.org\/isbn\/9781509055326","ISSN":"http:\/\/id.crossref.org\/issn\/1081-6011","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0750","series-title":"RIVER: A Binary Analysis Framework Using Symbolic Execution and Reversible x86 Instructions","isbn-type":"print","doi-asserted-by":"crossref","first-page":"779","DOI":"10.1007\/978-3-319-48989-6_50","volume":"vol. 9995","author":"Stoenescu","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319489889"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0755","isbn-type":"print","first-page":"301","article-title":"Extracting instruction semantics via symbolic execution of code generators","author":"Hasabnis","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450342186"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0760","isbn-type":"print","first-page":"117","article-title":"Software testing: a research travelogue (2000-2014)","author":"Orso","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450328654"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0765","first-page":"49","article-title":"Generating performance distributions via probabilistic symbolic execution","author":"Chen","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0770","isbn-type":"print","first-page":"105","article-title":"Quantifying information leaks using reliability analysis","author":"Phan","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450324526"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0775","isbn-type":"print","first-page":"131","article-title":"Model-counting approaches for nonlinear numerical constraints","author":"Borges","year":"2017","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319572888"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0780","isbn-type":"print","first-page":"166","article-title":"Probabilistic symbolic execution","author":"Geldenhuys","year":"2012","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450314541"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0785","first-page":"91","article-title":"An algorithmic theory of lattice points","volume":"vol. 38","author":"Barvinok","year":"1999"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0790","series-title":"Reliability analysis in symbolic PathFinder","isbn-type":"print","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1109\/ICSE.2013.6606608","author":"Filieri","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467330763","ISSN":"http:\/\/id.crossref.org\/issn\/0270-5257","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0795","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0800","isbn-type":"print","first-page":"437","article-title":"Statistical symbolic execution with informed sampling","author":"Filieri","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330565"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0805","isbn-type":"print","first-page":"575","article-title":"Exact and approximate probabilistic symbolic execution for nondeterministic programs","author":"Luckow","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450330138"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0810","series-title":"Rare Event Simulation Using Monte Carlo Methods","author":"Rubino","year":"2009"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0815","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1613\/jair.301","article-title":"Reinforcement learning: a survey","volume":"4","author":"Kaelbling","year":"1996","journal-title":"J. Artif. Intell. Res."},{"key":"10.1016\/bs.adcom.2018.10.002_bb0820","series-title":"A User's Guide for LattE Integrale v1.7.2","author":"Baldoni","year":"2014"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0825","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s00453-006-1231-0","article-title":"Counting integer points in parametric polytopes using Barvinok's rational functions","volume":"48","author":"Verdoolaege","year":"2007","journal-title":"Algorithmica","ISSN":"http:\/\/id.crossref.org\/issn\/0178-4617","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0830","isbn-type":"print","first-page":"123","article-title":"Compositional solution space quantification for probabilistic software analysis","author":"Borges","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327848"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0835","isbn-type":"print","first-page":"866","article-title":"Iterative distribution-aware sampling for probabilistic symbolic execution","author":"Borges","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336758"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0840","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/1132973.1132980","article-title":"Algorithm 852: realpaver: an interval solver using constraint satisfaction techniques","volume":"32","author":"Granvilliers","year":"2006","journal-title":"ACM Trans. Math. Softw.","ISSN":"http:\/\/id.crossref.org\/issn\/0098-3500","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0845","isbn-type":"print","first-page":"565","article-title":"A Model Counter for Constraints over Unbounded Strings","author":"Luu","year":"2014","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450327848"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0850","isbn-type":"print","first-page":"255","article-title":"Automata-based model counting for string constraints","author":"Aydin","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319216904"},{"issue":"8","key":"10.1016\/bs.adcom.2018.10.002_bb0855","doi-asserted-by":"crossref","first-page":"729","DOI":"10.1007\/s00236-017-0297-2","article-title":"Approximate counting in SMT and value estimation for probabilistic programs","volume":"54","author":"Chistikov","year":"2017","journal-title":"Acta Inform.","ISSN":"http:\/\/id.crossref.org\/issn\/1432-0525","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0860","series-title":"Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming","isbn-type":"print","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-642-40627-0_18","article-title":"A scalable approximate model counter","author":"Chakraborty","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9783642406270"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0865","first-page":"633","article-title":"Model counting","author":"Gomes","year":"2009"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0870","series-title":"Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-3-319-23404-5_15","article-title":"Model counting for complex data structures","volume":"vol. 9232","author":"Filieri","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319234038","ISSN":"http:\/\/id.crossref.org\/issn\/1611-3349","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0875","isbn-type":"print","first-page":"602","article-title":"Symbolic execution of programs with heap inputs","author":"Braione","year":"2015","ISBN":"http:\/\/id.crossref.org\/isbn\/9781450336758"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0880","series-title":"Deductive Software Verification\u2014the Key Book\u2014From Theory to Practice, Lecture Notes in Computer Science","isbn-type":"print","volume":"vol. 10001","year":"2016","ISBN":"http:\/\/id.crossref.org\/isbn\/9783319498119"},{"issue":"1","key":"10.1016\/bs.adcom.2018.10.002_bb0885","doi-asserted-by":"crossref","first-page":"2:1","DOI":"10.1145\/2110356.2110358","article-title":"The S2E platform: design, implementation, and applications","volume":"30","author":"Chipounov","year":"2012","journal-title":"ACM Trans. Comput. Syst.","ISSN":"http:\/\/id.crossref.org\/issn\/0734-2071","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0890","isbn-type":"print","first-page":"122","article-title":"Billions and billions of constraints: whitebox fuzz testing in production","author":"Bounimova","year":"2013","ISBN":"http:\/\/id.crossref.org\/isbn\/9781467330763"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0895","series-title":"Information Systems Security: 4th International Conference, ICISS 2008, Hyderabad, India, December 16\u201320, 2008. Proceedings","isbn-type":"print","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-89862-7_1","article-title":"BitBlaze: a new approach to computer security via binary analysis","author":"Song","year":"2008","ISBN":"http:\/\/id.crossref.org\/isbn\/9783540898627"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0900","doi-asserted-by":"crossref","DOI":"10.1109\/SP.2016.17","article-title":"SoK: (State of) the art of war: offensive techniques in binary analysis","author":"Shoshitaishvili","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0905","first-page":"31","article-title":"Triton: a dynamic symbolic execution framework","author":"Saudel","year":"2015"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0910","first-page":"442","article-title":"JDart: a dynamic symbolic analysis framework","volume":"vol. 9636","author":"Luckow","year":"2016"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0915","series-title":"CIVL: the concurrency intermediate verification language","author":"Siegel","year":"2014"},{"issue":"4","key":"10.1016\/bs.adcom.2018.10.002_bb0920","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/s10009-009-0118-1","article-title":"A survey of new trends in symbolic execution for software testing and analysis","volume":"11","author":"P\u0103s\u0103reanu","year":"2009","journal-title":"Int. J. Softw. Tools Technol. Transf.","ISSN":"http:\/\/id.crossref.org\/issn\/1433-2779","issn-type":"print"},{"issue":"2","key":"10.1016\/bs.adcom.2018.10.002_bb0925","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/2408776.2408795","article-title":"Symbolic execution for software testing: three decades later","volume":"56","author":"Cadar","year":"2013","journal-title":"Commun. ACM","ISSN":"http:\/\/id.crossref.org\/issn\/0001-0782","issn-type":"print"},{"issue":"7","key":"10.1016\/bs.adcom.2018.10.002_bb0930","doi-asserted-by":"crossref","first-page":"1758","DOI":"10.1016\/j.future.2012.02.006","article-title":"State of the art: dynamic symbolic execution for automated test generation","volume":"29","author":"Chen","year":"2013","journal-title":"Future Gener. Comput. Syst.","ISSN":"http:\/\/id.crossref.org\/issn\/0167-739X","issn-type":"print"},{"key":"10.1016\/bs.adcom.2018.10.002_bb0935","first-page":"1066","article-title":"Symbolic execution for software testing in practice: preliminary assessment","author":"Cadar","year":"2011"}],"container-title":["Advances in Computers"],"original-title":[],"link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0065245818300627?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0065245818300627?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,30]],"date-time":"2019-01-30T01:37:54Z","timestamp":1548812274000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0065245818300627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":186,"URL":"https:\/\/doi.org\/10.1016\/bs.adcom.2018.10.002","relation":{},"ISSN":["0065-2458"],"issn-type":[{"value":"0065-2458","type":"print"}],"subject":[],"published":{"date-parts":[[2019]]}}}