{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:29:36Z","timestamp":1770280176203,"version":"3.49.0"},"reference-count":45,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/ase.2017.8115634","type":"proceedings-article","created":{"date-parts":[[2017,11,23]],"date-time":"2017-11-23T17:03:57Z","timestamp":1511456637000},"page":"206-216","source":"Crossref","is-referenced-by-count":14,"title":["Modular verification of interrupt-driven software"],"prefix":"10.1109","author":[{"given":"Chungha","family":"Sung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Kusano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2875913.2875943"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2006.244049"},{"key":"ref33","first-page":"5","article-title":"Reduction of interrupt handler executions for model checking embedded software","author":"schlich","year":"2009","journal-title":"Haifa Verification Conference"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1113830.1113833"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086282"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_21"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2015.59"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950292"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926398"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786841"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092724"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106245"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1808266.1808278"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_36"},{"key":"ref14","year":"0","journal-title":"The intAbs tool and benchmark programs for evaluating intAbs"},{"key":"ref15","first-page":"297","article-title":"Model checking C program using F-Soft","author":"ivan?i?","year":"2005","journal-title":"International Conference on Computer Design"},{"key":"ref16","first-page":"661","article-title":"Apron: A library of numerical abstract domains for static analysis","author":"jeannet","year":"2009","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref17","first-page":"81","article-title":"Timing analysis of interrupt-driven programs under context bounds","author":"kotker","year":"2011","journal-title":"International Conference on Formal Methods In Computer-Aided Design"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2015.0360"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950291"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2017.02.002"},{"key":"ref4","first-page":"168","article-title":"A tool for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"International Conference on Tools and Algorithms for Construction and Analysis of Systems"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2011.04.054"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/24039.24041","article-title":"The program dependence graph and its use in optimization","volume":"9","author":"jeanne","year":"1987","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103693"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640108"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970332"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2003.1253196"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106243"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"ref21","first-page":"1","article-title":"Dzintars Avots, Michael Carbin, and Christopher Unkel. Context-sensitive program analysis as database queries","author":"lam","year":"2005","journal-title":"ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2914789"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_21"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996859"},{"key":"ref23","article-title":"Finding security vulnerabilities in Java applications with static analysis","author":"livshits","year":"2005","journal-title":"USENIX Security Symposium"},{"key":"ref44","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1109\/MEMCOD.2006.1695896","article-title":"Mixed symbolic representations for model checking software programs","author":"yang","year":"2006","journal-title":"Proc Int Conf Formal Methods Models Codesign"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/SERE-C.2013.33"},{"key":"ref25","first-page":"35","article-title":"Static analysis by abstract interpretation of sequential and multi-thread programs","author":"min\u00e9","year":"2012","journal-title":"Proc of the 10th School of Modelling and Verifying Parallel Processes"}],"event":{"name":"2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)","location":"Urbana, IL","start":{"date-parts":[[2017,10,30]]},"end":{"date-parts":[[2017,11,3]]}},"container-title":["2017 32nd IEEE\/ACM International Conference on Automated Software Engineering (ASE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8106906\/8115603\/08115634.pdf?arnumber=8115634","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T14:31:02Z","timestamp":1570372262000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8115634\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":45,"URL":"https:\/\/doi.org\/10.1109\/ase.2017.8115634","relation":{},"subject":[],"published":{"date-parts":[[2017,10]]}}}