{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:15:37Z","timestamp":1767928537113,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern computing systems have grown in complexity, and even though system components are generally carefully designed and even verified by different groups of people, the<jats:italic>composition<\/jats:italic>of these components is often regarded with less attention. Inconsistencies between components\u2019 assumptions on the rest of the system can have significant repercussions on this system, and may ultimately lead to safety or security issues. In this article, we introduce FreeSpec, a formalismbuilt upon the key idea that components can bemodeled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modeling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.<\/jats:p>","DOI":"10.1007\/s00165-020-00523-2","type":"journal-article","created":{"date-parts":[[2020,12,15]],"date-time":"2020-12-15T15:02:49Z","timestamp":1608044569000},"page":"127-150","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Modular verification of programs with effectsand effects handlers"],"prefix":"10.1145","volume":"33","author":[{"given":"Thomas","family":"Letan","sequence":"first","affiliation":[{"name":"Agence Nationale de la S\u00e9curit\u00e9 des Syst\u00e8mes d\u2019Information (ANSSI), Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0745-8730","authenticated-orcid":false,"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[{"name":"INRIA, Universit\u00e9 de Paris, CNRS, IRIF, F-75006, Paris, France"}]},{"given":"Pierre","family":"Chifflier","sequence":"additional","affiliation":[{"name":"Agence Nationale de la S\u00e9curit\u00e9 des Syst\u00e8mes d\u2019Information (ANSSI), Paris, France"}]},{"given":"Guillaume","family":"Hiet","sequence":"additional","affiliation":[{"name":"CentraleSup\u00e9lec, Inria, CNRS, IRISA, Rennes, France"}]}],"member":"320","reference":[{"key":"#cr-split#-e_1_2_1_2_1_2.1","doi-asserted-by":"crossref","unstructured":"Abel A Benke M Bove A Hughes J Norell U (2005) Verifying Haskell programs using constructive type theory. In: Leijen D","DOI":"10.1145\/1088348.1088355"},{"key":"#cr-split#-e_1_2_1_2_1_2.2","unstructured":"(ed) Proceedings of the ACM SIGPLAN workshop on Haskell Haskell 2005 Tallinn Estonia September 30 2005. ACM pp 62-73"},{"key":"e_1_2_1_2_2_2","volume-title":"The B-book: assigning programs to meanings","author":"Abrial J-R","year":"2005"},{"key":"e_1_2_1_2_3_2","unstructured":"Apfelmus H (2010) The operational package. https:\/\/hackage.haskell.org\/package\/operational"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"B\u00e9langer OS Appel AW (2017) Shrink fast correctly! In: Vanhoof W Pientka B (eds) Proceedings of the 19th international symposium on principles and practice of declarative programming Namur Belgium October 09\u201311 2017. ACM pp 49\u201360","DOI":"10.1145\/3131851.3131859"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_2_7_2","first-page":"330","article-title":"Coquet: a Coq library for verifying hardware","volume":"7086","author":"Thomas Braibant","year":"2011","journal-title":"CPP"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Brady E (2014) Resource-dependent algebraic effects. In: international symposium on trends in functional programming. Springer Berlin vol 8843 pp 18\u201333","DOI":"10.1007\/978-3-319-14675-1_2"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Claret G Yann R-G (2015) Mechanical verification of interactive programs specified by use cases. In: Proceedings of the third FME workshop on formal methods in software engineering. IEEE Press pp 61\u201367","DOI":"10.1109\/FormaliSE.2015.17"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Choi J Vijayaraghavan M Sherman B Chlipala A et al (2017) Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proceedings of the ACM on programming languages 1(ICFP):24","DOI":"10.1145\/3110268"},{"issue":"3","key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.22152\/programming-journal.org\/2019\/3\/8","article-title":"One Monad to prove them all","volume":"3","author":"Dylus S","year":"2019","journal-title":"Program J"},{"key":"e_1_2_1_2_12_2","unstructured":"DeepSpec. DeepSpec: The Science of Deep Specification"},{"key":"e_1_2_1_2_13_2","volume-title":"Getting into the SMRAM: SMM reloaded","author":"Duflot L","year":"2009"},{"issue":"4","key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2502508.2502520","article-title":"PLDI 2002: extended static checking for Java","volume":"48","author":"Flanagan C","year":"2013","journal-title":"SIGPLAN Not"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hur C-K Georg N Derek D Viktor V (2013) The power of parameterization in coinductive proof. In: Giacobazzi R Cousot R (eds) The 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages POPL '13 Rome Italy\u2014January 23\u201325 2013. ACM pp 193\u2013206","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Heyman T Scandariato R Joosen W (2012) 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 August 20\u201324 2012 pp 41\u201350","DOI":"10.1109\/WICSA-ECSA.212.12"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hinze R Voigtl\u00e4nder J(eds) (2015) Mathematics of program construction\u201412th international conference MPC 2015 K\u00f6nigswinter Germany June 29\u2013July 1 2015. Proceedings volume 9129 of Lecture notes in computer science. Springer Berlin","DOI":"10.1007\/978-3-319-19797-5"},{"key":"e_1_2_1_2_18_2","unstructured":"Inria. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_2_1_2_19_2","volume-title":"Software abstractions: logic, language and analysis","author":"Jackson D","year":"2012"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Jomaa N Nowak D Grimaud G Hym S (2016) Formal proof of dynamic memory isolation based on MMU. In: 2016 10th international symposium on theoretical aspects of software engineering (TASE). IEEE pp 73\u201380","DOI":"10.1109\/TASE.2016.28"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1145\/2887747.2804319","article-title":"Freer monads, more extensible effects","volume":"50","author":"Kiselyov O","year":"2015","journal-title":"ACM SIGPLAN notices. ACM"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Koh N Li Y Li Y Xia L Beringer L Honor\u00e9 W Mansky W Pierce BC Zdancewic S (2019) From C to interaction trees: specifying verifying and testing a networked server. In: Mahboubi A Myreen MO (eds) Proceedings of the 8th ACM SIGPLAN international conference on certified programs and proofs CPP 2019 Cascais Portugal January 14\u201315 2019 ACM pp 234\u2013248","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Letan T Chifflier P Hiet G N\u00e9ron P Morin B (2016) SpecCert: specifying and verifying hardware-based security enforcement. In: 21st international symposium on formal methods (FM 2016). Springer Berlin vol 9995","DOI":"10.1007\/978-3-319-48989-6_30"},{"key":"e_1_2_1_2_24_2","unstructured":"Letan T (2018) FreeSpec: a compositional reasoning framework for the Coq theorem prover https:\/\/github.com\/lthms\/speccert"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Liang S Hudak P Jones M (1995) Monadtrans formers and modular interpreters. In: Proceedings of the 22nd ACM SIGPLANSIGACT symposium on principles of programming languages. ACM pp 333\u2013343","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Letan T Yann R-G Pierre C Guillaume H (2018) Modular verification of programs with effects and effects handlers in Coq. In: 22st international symposium on formal methods (FM 2018). Springer Berlin vol 10951","DOI":"10.1007\/978-3-319-95582-7_20"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1145\/2345156.2254111","article-title":"RockSalt: better, faster, stronger SFI for the x86","volume":"47","author":"Morrisett G","year":"2012","journal-title":"ACMSIGPLAN notices. ACM"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1145\/1411203.1411237","article-title":"Y not: dependent types for imperative programs","volume":"43","author":"Nanevski A","year":"2008","journal-title":"ACM sigplan notices. ACM"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Odersky M Zenger M (2005) Scalable component abstractions. In: Johnson RE Gabriel RP (eds) Proceedings of the 20th annual ACM SIGPLAN conference on object-oriented programming systems languages and applications OOPSLA 2005 October 16\u201320 2005 San Diego CA USA. ACM pp 41\u201357","DOI":"10.1145\/1103845.1094815"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/357980.358011"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Pessaux F (2014) FoCaLiZe: inside an F-IDE. arXiv preprint arXiv:1404.6607","DOI":"10.4204\/EPTCS.149.7"},{"key":"e_1_2_1_2_34_2","unstructured":"Peyton Jones S (2001) Tackling the awkward squad: monadic input\/output concurrency exceptions and foreign-language calls in Haskell. Engineering theories of software construction"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for sharedmutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002) 22\u201325 July 2002 Copenhagen Denmark Proceedings. IEEE Computer Society pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Uustalu T (2017) Container combinatorics: monads and lax monoidal functors. In: Mousavi MR Sgall J (eds) Topics in theoretical computer science\u2014second IFIP WG 1.8 international conference TTCS 2017 Tehran Iran September 12\u201314 2017 Proceedings lecture notes in computer science. Springer Berlin vol 10608 pp 91\u2013105","DOI":"10.1007\/978-3-319-68953-1_8"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001560"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1109\/MSECP.2003.1253571","article-title":"A call to action: look beyond the horizon","volume":"6","author":"Wing JM","year":"2003","journal-title":"IEEE Secur Privacy"},{"key":"e_1_2_1_2_39_2","unstructured":"Wojtczuk R Rutkowska J (2009) Attacking SMM memory via intel CPU cache poisoning. Invisible Things Lab"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Xia L Zakowski Y He P Hur C-K Malecha G Pierce BC Zdancewic S (2019) Interaction trees: representing recursive and impure programs in Coq (work in progress). CoRR arXiv:1906.00046","DOI":"10.1145\/3371119"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00523-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-020-00523-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-020-00523-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-020-00523-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,5]],"date-time":"2022-12-05T02:50:45Z","timestamp":1670208645000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-020-00523-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2021,1]]}},"alternative-id":["10.1007\/s00165-020-00523-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-020-00523-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1]]},"assertion":[{"value":"8 July 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 October 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 December 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}