{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T16:58:25Z","timestamp":1774717105771,"version":"3.50.1"},"reference-count":78,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T026995\/1"],"award-info":[{"award-number":["EP\/T026995\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V000497\/1"],"award-info":[{"award-number":["EP\/V000497\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EU H2020 ELEGANT 957286"],"award-info":[{"award-number":["EU H2020 ELEGANT 957286"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Soteria Project Awarded by the U.K. Research and Innovation for the Digital Security by Design (DSbD) Programme"},{"DOI":"10.13039\/501100000770","name":"Dame Kathleen Ollerenshaw Fellowship of The University of Manchester","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000770","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2022]]},"DOI":"10.1109\/access.2022.3223359","type":"journal-article","created":{"date-parts":[[2022,11,18]],"date-time":"2022-11-18T20:42:34Z","timestamp":1668804154000},"page":"121365-121384","source":"Crossref","is-referenced-by-count":7,"title":["Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs"],"prefix":"10.1109","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7683-8182","authenticated-orcid":false,"given":"Fatimah K.","family":"Aljaafari","sequence":"first","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6102-4343","authenticated-orcid":false,"given":"Rafael","family":"Menezes","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0028-5440","authenticated-orcid":false,"given":"Edoardo","family":"Manino","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]},{"given":"Fedor","family":"Shmarov","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8772-8023","authenticated-orcid":false,"given":"Mustafa A.","family":"Mustafa","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6235-4272","authenticated-orcid":false,"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Manchester, Manchester, U.K"}]}],"member":"263","reference":[{"key":"ref73","doi-asserted-by":"publisher","DOI":"10.1145\/3434317"},{"key":"ref72","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468549"},{"key":"ref71","doi-asserted-by":"publisher","DOI":"10.1145\/3428298"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549110"},{"key":"ref76","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"ref39","year":"2022","journal-title":"Cseq"},{"key":"ref74","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454099"},{"key":"ref38","year":"2022","journal-title":"CSBMC Repository"},{"key":"ref75","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"ref78","author":"beyer","year":"2022","journal-title":"Violation Witnesses and Result Validation for Multi-Threaded Programs"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851830"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2007.370681"},{"key":"ref31","year":"2022","journal-title":"bzip2"},{"key":"ref30","year":"2022","journal-title":"pfscan"},{"key":"ref37","year":"2021","journal-title":"ESBMC Repository"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref35","author":"ben-ari","year":"2006","journal-title":"Principles of Concurrent and Distributed Programming"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274718"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99429-7_3"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"ref27","first-page":"712","article-title":"SATzilla-07: The design and analysis of an algorithm portfolio for sat","author":"xu","year":"2007","journal-title":"Principles and Practice of Constraint Programming"},{"key":"ref64","year":"2021","journal-title":"AFL Repository"},{"key":"ref65","article-title":"Personal communications","author":"lie","year":"2022"},{"key":"ref29","year":"2022","journal-title":"EBF Repository"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1186\/s42400-018-0002-y"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2016.23368"},{"key":"ref68","first-page":"745","article-title":"QSYM: A practical concolic execution engine tailored for hybrid fuzzing","author":"yun","year":"2018","journal-title":"Proc USENIX)"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510178"},{"key":"ref2","year":"2022","journal-title":"Multithreading Realtime Examples"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.75"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180251"},{"key":"ref22","author":"pak","year":"2012","journal-title":"Hybrid Fuzz Testing Discovering Software Bugs Via Fuzzing and Symbolic Execution"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/IWAST.2012.6228985"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3167132.3167289"},{"key":"ref23","first-page":"2325","article-title":"MUZZ: Thread-aware grey-box fuzzing for effective bug hunting in multithreaded programs","author":"chen","year":"2020","journal-title":"Proc 29th USENIX Secur Symp (USENIX Secur )"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_22"},{"key":"ref25","article-title":"FuSeBMC: A white-box fuzzer for finding security vulnerabilities in C programs","author":"alshmrany","year":"2020","journal-title":"Fundamental Approaches to Software Engineering"},{"key":"ref50","first-page":"28","article-title":"AddressSanitizer: A fast address sanity checker","author":"serebryany","year":"2012","journal-title":"Proc USENIX"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1791194.1791203"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_42"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_9"},{"key":"ref56","year":"2021","journal-title":"Mosquitto"},{"key":"ref55","year":"2021","journal-title":"wolfMQTT"},{"key":"ref54","year":"2022","journal-title":"Deagle"},{"key":"ref53","year":"2022","journal-title":"SV-COMP benchmarks"},{"key":"ref52","author":"maayan","year":"2021","journal-title":"SV-COMP Rules"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79379-1_6"},{"key":"ref11","article-title":"V-Fuzz: Vulnerability-oriented evolutionary fuzzing","author":"li","year":"2019","journal-title":"arXiv 1901 01142"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046745"},{"key":"ref13","first-page":"457","article-title":"Bounded model checking","author":"biere","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref14","first-page":"1","article-title":"ESBMC 6.1: Automated test case generation using bounded model checking","volume":"23","author":"gadelha","year":"2020","journal-title":"Int J Softw Tools Technol Transf"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454108"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_29"},{"key":"ref19","first-page":"1","article-title":"Symbolic execution of security protocol implementations: Handling cryptographic primitives","author":"vanhoef","year":"2018","journal-title":"Proc WOOT"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1346281.1346323"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1049\/iet-cps.2018.5006"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.09.005"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.3934"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790530"},{"key":"ref49","year":"2022","journal-title":"Declaring Attributes of Functions"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.391"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/195274.195295"},{"key":"ref46","year":"2022","journal-title":"AFLpluslus (Fast LLVM-Based)"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2022.24296"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1002\/9780470050118.ecse386"},{"key":"ref47","year":"2022","journal-title":"Fast LLVM-Based Instrumentation for AFL-Fuzz"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111379"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238176"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00078"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-15-0029-9_53"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/9668973\/09955513.pdf?arnumber=9955513","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,12]],"date-time":"2022-12-12T20:00:12Z","timestamp":1670875212000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9955513\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"references-count":78,"URL":"https:\/\/doi.org\/10.1109\/access.2022.3223359","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]}}}