{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:01:56Z","timestamp":1770296516607,"version":"3.49.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319955810","type":"print"},{"value":"9783319955827","type":"electronic"}],"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-95582-7_20","type":"book-chapter","created":{"date-parts":[[2018,7,11]],"date-time":"2018-07-11T10:31:17Z","timestamp":1531305077000},"page":"338-354","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Modular Verification of Programs with Effects and Effect Handlers in Coq"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Letan","sequence":"first","affiliation":[]},{"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Chifflier","sequence":"additional","affiliation":[]},{"given":"Guillaume","family":"Hiet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,12]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-319-48989-6_30","volume-title":"FM 2016: Formal Methods","author":"T Letan","year":"2016","unstructured":"Letan, T., Chifflier, P., Hiet, G., N\u00e9ron, P., Morin, B.: SpecCert: specifying and verifying hardware-based security enforcement. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 496\u2013512. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_30"},{"key":"20_CR2","unstructured":"Wojtczuk, R., Rutkowska, J.: Attacking SMM memory via Intel CPU cache poisoning. Invisible Things Lab (2009)"},{"key":"20_CR3","volume-title":"Getting into the SMRAM: SMM Reloaded","author":"L Duflot","year":"2009","unstructured":"Duflot, L., Levillain, O., Morin, B., Grumelard, O.: Getting into the SMRAM: SMM Reloaded. CanSecWest, Vancouver (2009)"},{"key":"20_CR4","unstructured":"Domas, C.: The memory sinkhole. In: BlackHat USA, July 2015"},{"key":"20_CR5","unstructured":"Kallenberg, C., Wojtczuk, R.: Speed racer: exploiting an intel flash protection race condition. Bromium Labs, January 2015"},{"key":"20_CR6","unstructured":"Kovah, X., Kallenberg, C., Butterworth, J., Cornwell, S.: SENTER Sandman: using Intel TXT to attack BIOSes. Hack in the Box (2015)"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-37300-8_2","volume-title":"Detection of Intrusions and Malware, and Vulnerability Assessment","author":"P Stewin","year":"2013","unstructured":"Stewin, P., Bystrov, I.: Understanding DMA malware. In: Flegel, U., Markatos, E., Robertson, W. (eds.) DIMVA 2012. LNCS, vol. 7591, pp. 21\u201341. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37300-8_2"},{"key":"20_CR8","unstructured":"Manual I.P.: Intel IA-64 Architecture Software Developer\u2019s Manual. Itanium Processor Microarchitecture Reference for Software Optimization, August 2000"},{"key":"20_CR9","unstructured":"Intel: Intel 5100 Memory Controller Hub Chipset"},{"issue":"OOPSLA","key":"20_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3133912","volume":"1","author":"Alastair Reid","year":"2017","unstructured":"Reid, A.: Who guards the guards? Formal validation of the Arm v8-M architecture specification. In: Proceedings of the ACM on Programming Languages, vol. 1(OOPSLA), p. 88 (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-21668-3_9","volume-title":"Computer Aided Verification","author":"R Leslie-Hurd","year":"2015","unstructured":"Leslie-Hurd, R., Caspi, D., Fernandez, M.: Verifying linearizability of Intel\u00ae software guard extensions. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 144\u2013160. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_9"},{"key":"20_CR12","unstructured":"Chong, S., Guttman, J., Datta, A., Myers, A., Pierce, B., Schaumont, P., Sherwood, T., Zeldovich, N.: Report on the NSF Workshop on Formal Methods for Security. ArXiv preprint arXiv:1608.00678 (2016)"},{"issue":"ICFP","key":"20_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110268","volume":"1","author":"Joonwon Choi","year":"2017","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A., et al.: Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of the ACM on Programming Languages, vol. 1(ICFP), p. 24 (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"20_CR14","unstructured":"Inria: The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-25379-9_24","volume-title":"Certified Programs and Proofs","author":"T Braibant","year":"2011","unstructured":"Braibant, T.: Coquet: a coq library for verifying hardware. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 330\u2013345. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_24"},{"issue":"6","key":"20_CR16","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1145\/2345156.2254111","volume":"47","author":"Greg Morrisett","year":"2012","unstructured":"Morrisett, G., Tan, G., Tassarotti, J., Tristan, J.B., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: ACM SIGPLAN Notices, vol. 47, pp. 395\u2013404. ACM (2012)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Jomaa, N., Nowak, D., Grimaud, G., Hym, S.: Formal proof of dynamic memory isolation based on MMU. In: 2016 10th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 73\u201380. IEEE (2016)","DOI":"10.1109\/TASE.2016.28"},{"issue":"1","key":"20_CR18","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1016\/j.jlamp.2014.02.001","volume":"84","author":"A Bauer","year":"2015","unstructured":"Bauer, A., Pretnar, M.: Programming with algebraic effects and handlers. J. Log. Algebraic Methods Program. 84(1), 108\u2013123 (2015)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"20_CR19","unstructured":"Apfelmus, H.: The operational package. https:\/\/hackage.haskell.org\/package\/operational"},{"key":"20_CR20","unstructured":"Hoareetal, C.: Tackling the awkward squad: monadic input\/output, concurrency, exceptions, and foreign-language calls in Haskell. Engineering Theories of Software Construction (2001)"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 333\u2013343. ACM (1995)","DOI":"10.1145\/199448.199528"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Heyman, T., Scandariato, R., Joosen, W.: Reusable formal models for secure software architectures. In: 2012 Joint Working IEEE\/IFIP Conference on Software Architecture and European Conference on Software Architecture, WICSA\/ECSA 2012, Helsinki, Finland, 20\u201324 August 2012, pp. 41\u201350 (2012)","DOI":"10.1109\/WICSA-ECSA.212.12"},{"key":"20_CR23","volume-title":"Software Abstractions: Logic, Language and Analysis","author":"D Jackson","year":"2012","unstructured":"Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2012)"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-14675-1_2","volume-title":"Trends in Functional Programming","author":"E Brady","year":"2015","unstructured":"Brady, E.: Resource-dependent algebraic effects. In: Hage, J., McCarthy, J. (eds.) TFP 2014. LNCS, vol. 8843, pp. 18\u201333. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-14675-1_2"},{"issue":"9","key":"20_CR25","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/1411203.1411237","volume":"43","author":"Aleksandar Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: ACM Sigplan Notices, vol. 43, pp. 229\u2013240. ACM (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Claret, G., R\u00e9gis-Gianas, Y.: Mechanical verification of interactive programs specified by use cases. In: Proceedings of the Third FME Workshop on Formal Methods in Software Engineering, pp. 61\u201367. IEEE Press (2015)","DOI":"10.1109\/FormaliSE.2015.17"},{"issue":"12","key":"20_CR27","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1145\/2887747.2804319","volume":"50","author":"Oleg Kiselyov","year":"2015","unstructured":"Kiselyov, O., Ishii, H.: Freer monads, more extensible effects. In: ACM SIGPLAN Notices, vol. 50, pp. 94\u2013105. ACM (2015)","journal-title":"ACM SIGPLAN Notices"},{"key":"20_CR28","volume-title":"The B-Book: Assigning Programs to Meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial, J.R., Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Pessaux, F.: FoCaLiZe: inside an F-IDE. ArXiv preprint arXiv:1404.6607 (2014)","DOI":"10.4204\/EPTCS.149.7"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-95582-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T12:29:54Z","timestamp":1571574594000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-95582-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319955810","9783319955827"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-95582-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}