{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:20:41Z","timestamp":1740122441598,"version":"3.37.3"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T00:00:00Z","timestamp":1600473600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T00:00:00Z","timestamp":1600473600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["CNS-1815883"],"award-info":[{"award-number":["CNS-1815883"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007245","name":"Microelectronics Advanced Research Corporation","doi-asserted-by":"publisher","award":["2018-TS-2846"],"award-info":[{"award-number":["2018-TS-2846"]}],"id":[{"id":"10.13039\/100007245","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10515-020-00276-5","type":"journal-article","created":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T03:57:31Z","timestamp":1600487851000},"page":"329-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analyzing system software components using API model guided symbolic execution"],"prefix":"10.1007","volume":"27","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5542-2142","authenticated-orcid":false,"given":"Tuba","family":"Yavuz","sequence":"first","affiliation":[]},{"given":"Ken","family":"Bai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,19]]},"reference":[{"key":"276_CR1","unstructured":"Amann, S., Nguyen, H.A., Nadi, S., Nguyen, T.N., Mezini, M.: A systematic evaluation of API-misuse detectors. CoRR arXiv:1712.00242 (2017)"},{"issue":"6","key":"276_CR2","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1109\/TSE.2017.2697848","volume":"44","author":"G Bai","year":"2018","unstructured":"Bai, G., Ye, Q., Wu, Y., Botha, H., Sun, J., Liu, Y., Dong, J.S., Visser, W.: Towards model checking android applications. IEEE Trans. Softw. Eng. 44(6), 595\u2013612 (2018)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"276_CR3","doi-asserted-by":"crossref","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with slam. Commun. ACM 54(7), 11 (2011)","DOI":"10.1145\/1965724.1965743"},{"key":"276_CR4","unstructured":"Ball, T., Rajamani, S.: Slic: A specification language for interface checking (of c). Tech. rep. (2002). https:\/\/tinyurl.com\/y8y4zkdy"},{"key":"276_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Computer Aided Verification\u201423rd International Conference, CAV\u201911. Proceedings, pp. 184\u2013190 (2011)","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"276_CR6","unstructured":"BlueBorne: https:\/\/info.armis.com\/rs\/645-PDC-047\/images\/BlueBorne%20Technical%20White%20Paper\\_20171130.pdf. Last accessed on August 1st, 2020"},{"key":"276_CR7","unstructured":"Bluetooth: Fix slab-out-of-bounds read in hci\\_extended\\_inquiry\\_result\\_evt(). https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/bluetooth\/bluetooth-next.git\/commit\/net\/bluetooth?id=51c19bf3d5cfaa66571e4b88ba2a6f6295311101. Last accessed on August 1st, 2020"},{"key":"276_CR8","unstructured":"Bluetooth: https:\/\/www.bluetooth.com\/. Last accessed on August 1st, 2020"},{"key":"276_CR9","unstructured":"BlueZ: Official Linux Bluetooth protocol stack. http:\/\/www.bluez.org\/. Last accessed on August 1st, 2020"},{"key":"276_CR10","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: Proceedings of the Sixth European Conference on Computer Systems, EuroSys 2011, Salzburg, Austria, April 10\u201313, pp. 183\u2013198 (2011)","DOI":"10.1145\/1966445.1966463"},{"key":"276_CR11","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8\u201310, 2008, San Diego, CA, USA, Proceedings, pp. 209\u2013224 (2008)"},{"key":"276_CR12","doi-asserted-by":"crossref","unstructured":"Cadar, C., Engler, D.: Execution generated test cases: how to make systems code crash itself. In: Proceedings of the 12th International Conference on Model Checking Software, SPIN\u201905 (2005)","DOI":"10.1007\/11537328_2"},{"issue":"2","key":"276_CR13","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"276_CR14","unstructured":"Carpenter, D.: Alsa: cs46xx: Potential null dereference in probe. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/stable\/linux.git\/commit\/sound\/pci\/cs46xx?id=1524f4e47f90b27a3ac84efbdd94c63172246a6f"},{"issue":"2","key":"276_CR15","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s10009-009-0098-1","volume":"11","author":"S Chatterjee","year":"2009","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamaric, Z.: A low-level memory model and an accompanying reachability predicate. Int. J. Softw. Tools Technol. Transf. 11(2), 105\u2013116 (2009)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"276_CR16","doi-asserted-by":"crossref","unstructured":"Chipounov, V., Kuznetsov, V., Candea, G.: The s2e platform: design, implementation, and applications. ACM Trans. Comput. Syst. 30(1) (2012)","DOI":"10.1145\/2110356.2110358"},{"key":"276_CR17","doi-asserted-by":"crossref","unstructured":"Fahl, S., Harbach, M., Perl, H., Koetter, M., Smith, M.: Rethinking SSL development in an applied world. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS \u201913 (2013)","DOI":"10.1145\/2508859.2516655"},{"key":"276_CR18","doi-asserted-by":"crossref","unstructured":"Georgiev, M., Iyengar, S., Jana, S., Anubhai, R., Boneh, D., Shmatikov, V.: The most dangerous code in the world: validating SSL certificates in non-browser software. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS \u201912 (2012)","DOI":"10.1145\/2382196.2382204"},{"key":"276_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12\u201315, 2005, pp. 213\u2013223 (2005)","DOI":"10.1145\/1064978.1065036"},{"key":"276_CR20","doi-asserted-by":"crossref","unstructured":"Heule, S., Sridharan, M., Chandra, S.: Mimic: Computing models for opaque code. In: Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2015 (2015)","DOI":"10.1145\/2786805.2786875"},{"key":"276_CR21","doi-asserted-by":"crossref","unstructured":"Indela, S., Kulkarni, M., Nayak, K., Dumitra\u015f, T.: Helping Johnny Encrypt: toward semantic interfaces for cryptographic frameworks. In: Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! (2016)","DOI":"10.1145\/2986012.2986024"},{"key":"276_CR22","unstructured":"KASAN: slab-out-of-bounds Read in hci\\_extended\\_inquiry\\_result\\_evt. https:\/\/syzkaller.appspot.com\/bug?id=4bf11aa05c4ca51ce0df86e500fce486552dc8d2. Last accessed on August 1st, 2020"},{"key":"276_CR23","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Pasareanu, C.S., Visser, W.: Generalized symbolic execution for model checking and testing. In: 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, pp. 553\u2013568 (2003)","DOI":"10.1007\/3-540-36577-X_40"},{"key":"276_CR24","doi-asserted-by":"crossref","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","DOI":"10.1145\/360248.360252"},{"key":"276_CR25","doi-asserted-by":"crossref","unstructured":"Mehlitz, P.C., Tkachuk, O., Ujma, M.: JPF-AWT: model checking GUI applications. In: 26th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2011), Lawrence, KS, USA, November 6\u201310, 2011, pp. 584\u2013587 (2011)","DOI":"10.1109\/ASE.2011.6100131"},{"key":"276_CR26","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/2896587","volume":"59","author":"BA Myers","year":"2016","unstructured":"Myers, B.A., Stylos, J.: Improving API usability. Commun. ACM 59, 6 (2016)","journal-title":"Commun. ACM"},{"key":"276_CR27","doi-asserted-by":"crossref","unstructured":"Nadi, S., Kr\u00fcger, S., Mezini, M., Bodden, E.: Jumping through hoops: why do java developers struggle with cryptography APIs? In: Proceedings of the 38th International Conference on Software Engineering, ICSE \u201916 (2016)","DOI":"10.1145\/2884781.2884790"},{"key":"276_CR28","doi-asserted-by":"crossref","unstructured":"Park, J., Jordan, A., Ryu, S.: Automatic modeling of opaque code for javascript static analysis. In: Fundamental Approaches to Software Engineering\u201422nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, pp. 43\u201360 (2019)","DOI":"10.1007\/978-3-030-16722-6_3"},{"key":"276_CR29","doi-asserted-by":"crossref","unstructured":"Qi, D., Sumner, W.N., Qin, F., Zheng, M., Zhang, X., Roychoudhury, A.: Modeling software execution environment. In: 19th Working Conference on Reverse Engineering, WCRE 2012, Kingston, ON, Canada, October 15\u201318, 2012, pp. 415\u2013424 (2012)","DOI":"10.1109\/WCRE.2012.51"},{"key":"276_CR30","unstructured":"Ramos, D.A., Engler, D.: Under-constrained symbolic execution: correctness checking for real code. In: Proceedings of the 24th USENIX Conference on Security Symposium, SEC\u201915, pp. 49\u201364 (2015)"},{"key":"276_CR31","doi-asserted-by":"crossref","unstructured":"Recoules, F., Bardin, S., Bonichon, R., Mounier, L., Potet, M.: Get rid of inline assembly through verification-oriented lifting. In: 34th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2019, San Diego, CA, USA, November 11\u201315, 2019, pp. 577\u2013589 (2019)","DOI":"10.1109\/ASE.2019.00060"},{"key":"276_CR32","unstructured":"Renzelmann, M.J., Kadav, A., Swift, M.M.: Symdrive: Testing drivers without devices. In: Thekkath, C., Vahdat, A. (eds.) 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8\u201310, 2012, pp. 279\u2013292. USENIX Association (2012)"},{"key":"276_CR33","doi-asserted-by":"crossref","unstructured":"Shi, K., Steinhardt, J., Liang, P.: Frangel: Component-based synthesis with control structures. Proc. ACM Program. Lang. 3(POPL) (2019)","DOI":"10.1145\/3290386"},{"key":"276_CR34","unstructured":"Syzkaller-Kernel Fuzzer: https:\/\/github.com\/google\/syzkaller. Last accessed on August 1st, 2020"},{"key":"276_CR35","doi-asserted-by":"crossref","unstructured":"Visser, W., Mehlitz, P.C.: Model checking programs with java pathfinder. In: Model Checking Software, 12th International SPIN Workshop, San Francisco, CA, USA, August 22\u201324, 2005, Proceedings, p.\u00a027 (2005)","DOI":"10.1007\/11537328_5"},{"key":"276_CR36","doi-asserted-by":"crossref","unstructured":"Wang, W., Barrett, C.W., Wies, T.: Partitioned memory models for program analysis. In: Verification, Model Checking, and Abstract Interpretation\u201418th International Conference, VMCAI 2017, Paris, France, January 15\u201317, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10145, pp. 539\u2013558. Springer (2017)","DOI":"10.1007\/978-3-319-52234-0_29"},{"key":"276_CR37","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent linux device drivers. In: 22nd IEEE\/ACM International Conference on Automated Software Engineering (ASE 2007), November 5\u20139, 2007, Atlanta, GA, USA, pp. 501\u2013504 (2007)"},{"key":"276_CR38","unstructured":"Yavuz, T.: [patch] net: hso: do not call unregister if not registered. https:\/\/lists.openwall.net\/netdev\/2019\/02\/09\/1 (2019)"},{"key":"276_CR39","doi-asserted-by":"crossref","unstructured":"Yong, S.H., Horwitz, S., Reps, T.: Pointer analysis for programs with structures and casting. In: Proceedings of the ACM SIGPLAN 1999 Conference on Programming Language Design and Implementation, PLDI \u201999, pp. 91\u2013103. Association for Computing Machinery, New York, NY, USA (1999)","DOI":"10.1145\/301618.301647"},{"key":"276_CR40","unstructured":"Yun, I., Min, C., Si, X., Jang, Y., Kim, T., Naik, M.: APISan: sanitizing API usages through semantic cross-checking. In: 25th USENIX Security Symposium, USENIX Security\u201916, pp. 363\u2013378 (2016)"},{"issue":"1","key":"276_CR41","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1134\/S0361768815010065","volume":"41","author":"IS Zakharov","year":"2015","unstructured":"Zakharov, I.S., Mandrykin, M.U., Mutilin, V.S., Novikov, E., Petrenko, A.K., Khoroshilov, A.V.: Configurable toolset for static verification of operating systems kernel modules. Program. Comput. Softw. 41(1), 49\u201364 (2015)","journal-title":"Program. Comput. Softw."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-020-00276-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10515-020-00276-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-020-00276-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,18]],"date-time":"2021-09-18T23:29:08Z","timestamp":1632007748000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10515-020-00276-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,19]]},"references-count":41,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["276"],"URL":"https:\/\/doi.org\/10.1007\/s10515-020-00276-5","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"type":"print","value":"0928-8910"},{"type":"electronic","value":"1573-7535"}],"subject":[],"published":{"date-parts":[[2020,9,19]]},"assertion":[{"value":"11 January 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 September 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 September 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}