{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:38:24Z","timestamp":1759333104752,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,12,7]],"date-time":"2017-12-07T00:00:00Z","timestamp":1512604800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Intel Corporation for research on Effective Validation of Firmware"},{"name":"SRC","award":["2012-TJ-2269 and 2016-CT-2707"],"award-info":[{"award-number":["2012-TJ-2269 and 2016-CT-2707"]}]},{"name":"ERC project","award":["280053 \u201cCPROVER\u201d"],"award-info":[{"award-number":["280053 \u201cCPROVER\u201d"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/H017585\/1"],"award-info":[{"award-number":["EP\/H017585\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Artemis Joint Undertaking","award":["295311"],"award-info":[{"award-number":["295311"]}]},{"name":"VeTeSS: Verification and Testing to Support Functional Safety Standards"},{"name":"H2020 FET OPEN","award":["712689 SC2"],"award-info":[{"award-number":["712689 SC2"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>Interrupt-driven software is difficult to test and debug, especially when interrupts can be nested and subject to priorities. Interrupts can arrive at arbitrary times, leading to an exponential blow-up in the number of cases to consider. We present a new formal approach to verifying interrupt-driven software based on symbolic execution. The approach leverages recent advances in the encoding of the execution traces of interacting, concurrent threads. We assess the performance of our method on benchmarks drawn from embedded systems code and device drivers, and experimentally compare it to conventional approaches that use source-to-source transformations. Our results show that our method significantly outperforms these techniques. To the best of our knowledge, our work is the first to demonstrate effective verification of low-level embedded software with nested interrupts.<\/jats:p>","DOI":"10.1145\/3147432","type":"journal-article","created":{"date-parts":[[2017,12,11]],"date-time":"2017-12-11T13:26:47Z","timestamp":1512998807000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Effective Verification for Low-Level Software with Competing Interrupts"],"prefix":"10.1145","volume":"17","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5055-5202","authenticated-orcid":false,"given":"Lihao","family":"Liang","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, UK"}]},{"given":"Tom","family":"Melham","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[{"name":"University of Sussex, Falmer, Brighton, UK"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, London, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,12,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_21"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_12"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_4"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2011.04.054"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734089"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Edmund M. Clarke Orna Grumberg and Doron Peled. 2001. Model Checking. MIT Press.  Edmund M. Clarke Orna Grumberg and Doron Peled. 2001. Model Checking. MIT Press.","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_40"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_34"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 3rd International Workshop on Computer Aided Verification (LNCS)","volume":"575","author":"Godefroid Patrice","year":"1991","unstructured":"Patrice Godefroid and Pierre Wolper . 1991 . Using partial orders for the efficient verification of deadlock freedom and safety properties . In Proceedings of the 3rd International Workshop on Computer Aided Verification (LNCS) , Vol. 575 . Springer, 332--342. Patrice Godefroid and Pierre Wolper. 1991. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the 3rd International Workshop on Computer Aided Verification (LNCS), Vol. 575. Springer, 332--342."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.108"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency (LNCS)","volume":"354","author":"Katz Shmuel","year":"1988","unstructured":"Shmuel Katz and Doron Peled . 1988 . An efficient verification method for parallel and distributed programs . In Proceedings of the Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency (LNCS) , Vol. 354 . Springer, 489--507. Shmuel Katz and Doron Peled. 1988. An efficient verification method for parallel and distributed programs. In Proceedings of the Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency (LNCS), Vol. 354. Springer, 489--507."},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the 17th International SPIN Workshop on Model Checking Software (LNCS)","volume":"6349","author":"Kidd Nicholas","year":"2010","unstructured":"Nicholas Kidd , Suresh Jagannathan , and Jan Vitek . 2010 . One stack to run them all -- Reducing concurrent analysis to sequential analysis under priority scheduling . In Proceedings of the 17th International SPIN Workshop on Model Checking Software (LNCS) , Vol. 6349 . Springer, 245--261. Nicholas Kidd, Suresh Jagannathan, and Jan Vitek. 2010. One stack to run them all -- Reducing concurrent analysis to sequential analysis under priority scheduling. In Proceedings of the 17th International SPIN Workshop on Model Checking Software (LNCS), Vol. 6349. Springer, 245--261."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.599898"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LES.2013.2276434"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_48"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS)","volume":"8413","author":"Morse Jeremy","year":"2014","unstructured":"Jeremy Morse , Mikhail Ramalho , Lucas C. Cordeiro , Denis Nicole , and Bernd Fischer . 2014 . ESBMC 1.22 (competition contribution) . In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS) , Vol. 8413 . Springer, 405--407. Jeremy Morse, Mikhail Ramalho, Lucas C. Cordeiro, Denis Nicole, and Bernd Fischer. 2014. ESBMC 1.22 (competition contribution). In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (LNCS), Vol. 8413. Springer, 405--407."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.07.030"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735529"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_51"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 5th International Haifa Verification Conference on Hardware and Software: Verification and Testing (LNCS)","volume":"6405","author":"Schlich Bastian","year":"2009","unstructured":"Bastian Schlich , Thomas Noll , J\u00f6rg Brauer , and Lucas Brutschy . 2009 . Reduction of interrupt handler executions for model checking embedded software . In Proceedings of the 5th International Haifa Verification Conference on Hardware and Software: Verification and Testing (LNCS) , Vol. 6405 . Springer, 5--20. Bastian Schlich, Thomas Noll, J\u00f6rg Brauer, and Lucas Brutschy. 2009. Reduction of interrupt handler executions for model checking embedded software. In Proceedings of the 5th International Haifa Verification Conference on Hardware and Software: Verification and Testing (LNCS), Vol. 6405. Springer, 5--20."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_39"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882301"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926433"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2015.59"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321719"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SERE-C.2013.33"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147432","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3147432","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:16Z","timestamp":1750212676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147432"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,7]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3147432"],"URL":"https:\/\/doi.org\/10.1145\/3147432","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2017,12,7]]},"assertion":[{"value":"2016-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}