{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T15:28:54Z","timestamp":1749223734146,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948201"},{"type":"electronic","value":"9783319948218"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94821-8_1","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Physical Addressing on Real Hardware in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Reto","family":"Achermann","sequence":"first","affiliation":[]},{"given":"Lukas","family":"Humbel","sequence":"additional","affiliation":[]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[]},{"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"1_CR1","unstructured":"Achermann, R.: Message passing and bulk transport on heterogenous multiprocessors. Master\u2019s thesis, Department of Computer Science, ETH Zurich, Switzerland (2017)"},{"key":"1_CR2","unstructured":"Achermann, R., Cock, D., Humebl, L.: Hardware Models in Isabelle\/HOL, January 2018. https:\/\/github.com\/BarrelfishOS\/Isabelle-hardware-models"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Achermann, R., Humbel, L., Cock, D., Roscoe, T.: Formalizing memory accesses and interrupts. In: Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017, pp. 66\u2013116 (2017)","DOI":"10.4204\/EPTCS.244.4"},{"issue":"2","key":"1_CR4","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/s10703-012-0161-5","volume":"41","author":"J Alglave","year":"2012","unstructured":"Alglave, J.: A formal hierarchy of weak memory models. Form. Methods Syst. Des. 41(2), 178\u2013210 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"1_CR5","unstructured":"The Barrelfish Operating System. https:\/\/www.barrelfish.org"},{"issue":"4","key":"1_CR6","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D., Paul, W.J.: Putting it all together \u2013 formal verification of the VAMP. Int. J. Softw. Tools Technol. Transf. 8(4), 411\u2013430 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"1_CR7","unstructured":"Bishop, M.K., Brock, C., Hunt, W.A.: The FM9001 Microprocessor Proof. Technical report 86, Computational Logic Inc. (1994)"},{"key":"1_CR8","unstructured":"devicetree.org: Devicetree Specification, May 2016. Release 0.1. http:\/\/www.devicetree.org\/specifications-pdf"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Flur, S., Gray, K.E., Pulte, C., Sarkar, S., Sezgin, A., Maranget, L., Deacon, W., Sewell, P.: Modelling the ARMv8 architecture, operationally: concurrency and ISA. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 608\u2013621. ACM, St. Petersburg (2016)","DOI":"10.1145\/2837614.2837615"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243\u2013258. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_18"},{"key":"1_CR11","unstructured":"Gerber, S., Zellweger, G., Achermann, R., Kourtis, K., Roscoe, T., Milojicic, D.: Not your parents\u2019 physical address space. In: Proceedings of the 15th USENIX Conference on Hot Topics in Operating Systems, HOTOS 2015, p. 16 (2015)"},{"key":"1_CR12","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj\u00f6berg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI 2016, pp. 653\u2013669. USENIX Association, Savannah (2016)"},{"issue":"2104","key":"1_CR13","doi-asserted-by":"publisher","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","volume":"375","author":"WA Hunt","year":"2017","unstructured":"Hunt, W.A., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Phil. Trans. R. Soc. A 375(2104), 20150399 (2017)","journal-title":"Phil. Trans. R. Soc. A"},{"key":"1_CR14","unstructured":"Integrated Device Technology, Inc.: IDT79R4600 TM and IDT79R4700 TM RISC Processor Hardware User\u2019s Manual, revision 2.0 edition, April 1995"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP 2009, pp. 207\u2013220. ACM, Big Sky (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Kocher, P., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints, January 2018","DOI":"10.1109\/SP.2019.00002"},{"key":"1_CR17","unstructured":"Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown. ArXiv e-prints, January 2018"},{"key":"1_CR18","unstructured":"T.B. Project: Sockeye in Barrelfish"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Reid, A.: Trustworthy specifications of ARM V8-A and V8-M system level architecture. In: FMCAD 2016, pp. 161\u2013168. FMCAD Inc., Austin (2016)","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"1_CR20","unstructured":"Schwyn, D.: Hardware configuration with dynamically-queried formal models. Master\u2019s thesis, Department of Computer Science, ETH Zurich, Switzerland (2017)"},{"key":"1_CR21","unstructured":"Texas Instruments: OMAP44xx Multimedia Device Technical Reference Manual, April 2014. Version AB. www.ti.com\/lit\/ug\/swpu235ab\/swpu235ab.pdf"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T05:01:28Z","timestamp":1571547688000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}