{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:43Z","timestamp":1763467903444},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2009,3,20]],"date-time":"2009-03-20T00:00:00Z","timestamp":1237507200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10817-009-9118-9","type":"journal-article","created":{"date-parts":[[2009,3,19]],"date-time":"2009-03-19T10:02:50Z","timestamp":1237456970000},"page":"301-347","source":"Crossref","is-referenced-by-count":24,"title":["Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads"],"prefix":"10.1007","volume":"42","author":[{"given":"Xinyu","family":"Feng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,20]]},"reference":[{"key":"9118_CR1","doi-asserted-by":"crossref","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: Proc. 4th International Symposium on Formal Methods for Components and Objects (FMCO\u201905). LNCS, vol. 4111, pp. 115\u2013137. Springer, New York (2005)","DOI":"10.1007\/11804192_6"},{"issue":"11","key":"9118_CR2","doi-asserted-by":"crossref","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: a study in operating system verification. IEEE Trans. Softw. Eng. 15(11), 1382\u20131396 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9118_CR3","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proc. 32nd ACM Symp. on Principles of Prog. Lang., pp. 259\u2013270. ACM, New York (2005)","DOI":"10.1145\/1040305.1040327"},{"issue":"2","key":"9118_CR4","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1109\/TSE.1975.6312840","volume":"1","author":"P Brinch Hansen","year":"1975","unstructured":"Brinch Hansen, P.: The programming language concurrent pascal. IEEE Trans. Software Eng. 1(2), 199\u2013207 (1975)","journal-title":"IEEE Trans. Software Eng."},{"key":"9118_CR5","doi-asserted-by":"crossref","unstructured":"Brookes, S.: A semantics for concurrent separation logic. In: Proc. 15th Int\u2019l Conf. on Concurrency Theory (CONCUR\u201904). LNCS, vol. 3170, pp. 16\u201334. Springer, New York (2004)","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"9118_CR6","unstructured":"Coq Development Team: The Coq proof assistant reference manual. The Coq release v8.1 (2006)"},{"key":"9118_CR7","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pp. 59\u201369. ACM, New York (2001)","DOI":"10.1145\/378795.378811"},{"key":"9118_CR8","doi-asserted-by":"crossref","unstructured":"Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: Proc. 16th European Symp. on Prog. (ESOP\u201907). LNCS, vol.\u00a04421, pp. 173\u2013188. Springer, New York (2007)","DOI":"10.1007\/978-3-540-71316-6_13"},{"key":"9118_CR9","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proc. 2007 ACM Workshop on Types in Lang. Design and Impl., pp. 67\u201378. ACM, New York (2007)","DOI":"10.1145\/1190315.1190325"},{"key":"9118_CR10","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z.: Modular verification of concurrent assembly code with dynamic thread creation and termination. In: Proc. 2005 ACM Int\u2019l Conf. on Functional Prog., pp. 254\u2013267. ACM, New York (2005)","DOI":"10.1145\/1086365.1086399"},{"key":"9118_CR11","unstructured":"Feng, X., Shao, Z.: Local reasoning and information hiding in SCAP. Tech. rep. YALEU\/DCS\/TR-1398, Dept. of Computer Science, Yale University, New Haven, CT (2008). http:\/\/flint.cs.yale.edu\/publications\/SCAPFrame.html"},{"key":"9118_CR12","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems. In: Proc. Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE\u201908). LNCS, vol. 5295, pp. 54\u201369. Springer, New York (2008)","DOI":"10.1007\/978-3-540-87873-5_8"},{"key":"9118_CR13","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Proc. 2006 ACM Conf. on Prog. Lang. Design and Impl., pp.\u00a0401\u2013414. ACM, New York (2006)","DOI":"10.1145\/1133981.1134028"},{"key":"9118_CR14","doi-asserted-by":"crossref","unstructured":"Gargano, M., Hillebrand, M.A., Leinenbach, D., Paul, W.J.: On the correctness of operating system kernels. In: Proc. 18th Int\u2019l Conf. on Theorem Proving in Higher Order Logics. LNCS, vol. 3603, pp. 1\u201316. Springer, New York (2005)","DOI":"10.1007\/11541868_1"},{"key":"9118_CR15","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Proc. Fifth ASIAN Symp. on Prog. Lang. and Sys. (APLAS\u201907). LNCS, vol.\u00a04807, pp. 19\u201337. Springer, New York (2007)","DOI":"10.1007\/978-3-540-76637-7_3"},{"issue":"1","key":"9118_CR16","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/357980.358001","volume":"26","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 26(1), 53\u201356 (1969)","journal-title":"Commun. ACM"},{"key":"9118_CR17","first-page":"61","volume-title":"Operating Systems Techniques","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating Systems Techniques, pp. 61\u201371. Academic, London (1972)"},{"issue":"10","key":"9118_CR18","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"CAR Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: An operating system structuring concept. Commun. ACM 17(10), 549\u2013557 (1974)","journal-title":"Commun. ACM"},{"key":"9118_CR19","doi-asserted-by":"crossref","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: Proc. 17th European Symp. on Prog. (ESOP\u201908). LNCS, vol. 4960, pp. 353\u2013367. Springer, New York (2008)","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"9118_CR20","unstructured":"Hunt, G.C., Larus, J.R.: Singularity design motivation. Tech. rep. MSR-TR-2004-105, Microsoft Corporation (2004)"},{"key":"9118_CR21","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM Symp. on Principles of Prog. Lang., pp. 14\u201326. ACM, New York (2001)","DOI":"10.1145\/360204.375719"},{"issue":"4","key":"9118_CR22","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9118_CR23","doi-asserted-by":"crossref","unstructured":"Kleymann, T.: Metatheory of verification calculi in LEGO\u2014to what extent does syntax matter? In: Proc. International Workshop on Types for Proofs and Programs (TYPES\u201998). LNCS, vol.\u00a01657, pp. 133\u2013148. Springer, New York (1998)","DOI":"10.1007\/3-540-48167-2_10"},{"issue":"2","key":"9118_CR24","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1145\/358818.358824","volume":"23","author":"BW Lampson","year":"1980","unstructured":"Lampson, B.W., Redell, D.D.: Experience with processes and monitors in Mesa. Commun. ACM 23(2), 105\u2013117 (1980)","journal-title":"Commun. ACM"},{"key":"9118_CR25","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Proc. 2007 ACM Conf. on Prog. Lang. Design and Impl., pp. 468\u2013479. ACM, New York (2007)","DOI":"10.1145\/1250734.1250788"},{"key":"9118_CR26","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. In: Proc. 25th ACM Symp. on Principles of Prog. Lang., pp. 85\u201397. ACM, New York (1998)","DOI":"10.1145\/268946.268954"},{"key":"9118_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Dutertre, B., Shankar, N.: A tutorial on satisfiability modulo theories. In: Proc. 19th International Conference on Computer Aided Verification (CAV\u201907). LNCS, vol.\u00a04590, pp.\u00a020\u201336. Springer, New York (2007)","DOI":"10.1007\/978-3-540-73368-3_5"},{"key":"9118_CR28","doi-asserted-by":"crossref","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: machine context management. In: Proc. 20th Int\u2019l Conf. on Theorem Proving in Higher Order Logics. LNCS, vol. 4421, pp. 189\u2013206. Springer, New York (2007)","DOI":"10.1007\/978-3-540-74591-4_15"},{"key":"9118_CR29","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Proc. 15th Int\u2019l Conf. on Concurrency Theory (CONCUR\u201904). LNCS, vol. 3170, pp. 49\u201367. Springer, New York (2004)","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"9118_CR30","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proc. 31th ACM Symp. on Principles of Prog. Lang., pp. 268\u2013280. ACM, New York (2004)","DOI":"10.1145\/982962.964024"},{"key":"9118_CR31","doi-asserted-by":"crossref","unstructured":"Palsberg, J., Ma, D.: A typed interrupt calculus. In: Proc. 7th Int\u2019l Symp. on Formal Tech. in Real-Time and Fault-Tolerant Sys. (FTRTFT\u201902). LNCS, vol. 2469, pp. 291\u2013310. Springer, New York (2002)","DOI":"10.1007\/3-540-45739-9_18"},{"key":"9118_CR32","unstructured":"Paul, W., Broy, M., In der Rieden, T.: The Verisoft XT project. http:\/\/www.verisoft.de (2007)"},{"key":"9118_CR33","doi-asserted-by":"crossref","unstructured":"Regehr, J., Cooprider, N.: Interrupt verification via thread verification. Electron. Notes Theor. Comput. Sci. 174(9) (2007)","DOI":"10.1016\/j.entcs.2007.04.002"},{"key":"9118_CR34","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th Annual IEEE Symp. on Logic in Comp. Sci. (LICS\u201902), pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"9118_CR35","doi-asserted-by":"crossref","unstructured":"Suenaga, K., Kobayashi, N.: Type based analysis of deadlock for a concurrent calculus with interrupts. In: Proc. 16th European Symp. on Prog. (ESOP\u201907). LNCS, vol. 4421, pp. 490\u2013504. Springer, New York (2007)","DOI":"10.1007\/978-3-540-71316-6_33"},{"key":"9118_CR36","unstructured":"Tuch, H., Klein, G., Heiser, G.: OS verification\u2014now! In: Proc. 10th Workshop on Hot Topics in Operating Systems, Santa Fe, 12\u201315 June 2005"},{"key":"9118_CR37","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Proc. 18th Int\u2019l Conf. on Concurrency Theory (CONCUR\u201907). LNCS, vol. 4703, pp. 256\u2013271. Springer, New York (2007)","DOI":"10.1007\/978-3-540-74407-8_18"},{"issue":"1","key":"9118_CR38","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."},{"key":"9118_CR39","doi-asserted-by":"crossref","unstructured":"Yang, H., O\u2019Hearn, P.W.: A semantic basis for local reasoning. In: Proc. 5th Int\u2019l Conf. on Foundations of Software Science and Computation Structures (FoSSaCS\u201902). LNCS, vol. 2303, pp. 402\u2013416. Springer, New York (2002)","DOI":"10.1007\/3-540-45931-6_28"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9118-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9118-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9118-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:48Z","timestamp":1559265708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9118-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,3,20]]},"references-count":39,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["9118"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9118-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,20]]}}}