{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:26:33Z","timestamp":1768213593618,"version":"3.49.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_10","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:51Z","timestamp":1768202511000},"page":"197-211","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Try-Mopsa: Relational Static Analysis in\u00a0Your Pocket"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8487-0326","authenticated-orcid":false,"given":"Rapha\u00ebl","family":"Monat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"10_CR1","unstructured":"Alt-Ergo Developers. Try Alt-Ergo. URL: https:\/\/alt-ergo.ocamlpro.com\/try.html"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Emilio Jes\u00fas Gallego Arias, Beno\u00eet Pin, and Pierre Jouvelot. \u201cjsCoq: Towards Hybrid Theorem Proving Interfaces\u201d. In: UITP. 2016. https:\/\/doi.org\/10.4204\/EPTCS.239.2","DOI":"10.4204\/EPTCS.239.2"},{"key":"10_CR3","unstructured":"Benedikt Becker, Jean-Christophe Filli\u00e2tre, Nguyen Kim, Claude March\u00e9, Guillaume Melquiond, Andrei Paskevich, and Patault Paul. Try Why3. 2025. URL: https:\/\/www.why3.org\/try\/"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Dirk Beyer. \u201cCompetition on Software Verification and Witness Validation: SV-COMP 2023\u201d. In: TACAS. 2023. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Sylvain Boulm\u00e9, Alexandre Mar\u00e9chal, DavidMonniaux, Micha\u00ebl P\u00e9rin, and Hang Yu. \u201cThe Verified Polyhedron Library: an Overview\u201d. In: SYNASC. 2018. https:\/\/doi.org\/10.1109\/SYNASC.2018.00014","DOI":"10.1109\/SYNASC.2018.00014"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"Benjamin Canou, Roberto Di Cosmo, and Gr\u00e9goire Henry. \u201cScaling up functional programming education: under the hood of the OCaml MOOC\u201d. In: Proc. ACM Program. Lang. ICFP (2017). https:\/\/doi.org\/10.1145\/3110248","DOI":"10.1145\/3110248"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Maria Christakis and Christian Bird. \u201cWhat developers want and need from program analysis: an empirical study\u201d. In: ASE. 2016. https:\/\/doi.org\/10.1145\/2970276.2970347","DOI":"10.1145\/2970276.2970347"},{"key":"10_CR8","unstructured":"Sylvain Conchon, Albin Coquereau, Mohamed Iguernlala, and Alain Mebsout. \u201cAlt-Ergo 2.2\u201d. In: SMT Workshop. Oxford, United Kingdom, July 2018. URL: https:\/\/inria.hal.science\/hal-01960203"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Lo\u00efc Correnson. \u201cIvette: A Modern GUI for Frama-C\u201d. In: SEFM. 2022. https:\/\/doi.org\/10.1007\/978-3-031-26236-4_10","DOI":"10.1007\/978-3-031-26236-4_10"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. \u201cAbstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints\u201d. In: POPL. 1977. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Nicolas Halbwachs. \u201cAutomatic Discovery of Linear Restraints Among Variables of a Program\u201d. In: POPL. 1978. https:\/\/doi.org\/10.1145\/512760.512770","DOI":"10.1145\/512760.512770"},{"key":"10_CR12","unstructured":"Albert Danial. cloc: v2.06. June 2025. URL: https:\/\/github.com\/AlDanial\/cloc\/"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Adel Djoudi and S\u00e9bastien Bardin. \u201cBINSEC: Binary Code Analysis with Low-Level Regions\u201d. In: TACAS. 2015. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_17","DOI":"10.1007\/978-3-662-46681-0_17"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Lisa Nguyen Quang Do, Stefan Kr\u00fcger, Patrick Hill, Karim Ali, and Eric Bodden. \u201cDebugging Static Analysis\u201d. In: IEEE Trans. Software Eng. 7 (2020). https:\/\/doi.org\/10.1109\/TSE.2018.2868349","DOI":"10.1109\/TSE.2018.2868349"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Lisa Nguyen Quang Do, James R. Wright, and Karim Ali. \u201cWhy Do Software Developers Use Static Analysis Tools? A User-Centered Study of Developer Needs and Motivations\u201d. In: IEEE Trans. Software Eng. 3 (2022). https:\/\/doi.org\/10.1109\/TSE.2020.3004525","DOI":"10.1109\/TSE.2020.3004525"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Daniela Ferreiro, Jos\u00e9 F. Morales, Salvador Abreu, and Manuel V. Hermenegildo. \u201cDemonstrating (Hybrid) Active Logic Documents and the Ciao Prolog Playground, and an Application to Verification Tutorials\u201d. In: ICLP. 2023. https:\/\/doi.org\/10.4204\/EPTCS.385.33","DOI":"10.4204\/EPTCS.385.33"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"Jean-Christophe Filli\u00e2tre and Andrei Paskevich. \u201cWhy3 - Where Programs Meet Provers\u201d. In: ESOP. 2013. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, and Shmuel Sagiv. \u201cNumeric Domains with Summarized Dimensions\u201d. In: TACAS. 2004. https:\/\/doi.org\/10.1007\/978-3-540-24730-2_38","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Karoliine Holter, Juhan Oskar Hennoste, Patrick Lam, Simmo Saan, and Vesal Vojdani. \u201cAbstract Debuggers: Exploring Program Behaviors using Static Analysis Results\u201d. In: Onward! 2024. https:\/\/doi.org\/10.1145\/3689492.3690053","DOI":"10.1145\/3689492.3690053"},{"key":"10_CR20","unstructured":"Jane Street Group, LLC. JavaScript stubs for the Zarith Library. Version 0.17.0. July 2024. URL: https:\/\/github.com\/janestreet\/zarith_stubs_js"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Bertrand Jeannet. \u201cRelational interprocedural verification of concurrent programs\u201d. In: Softw. Syst. Model. 2 (2013). https:\/\/doi.org\/10.1007\/S10270-012-0230-7","DOI":"10.1007\/S10270-012-0230-7"},{"key":"10_CR22","unstructured":"Bertrand Jeannet. Web Interface for the Interproc Analyzer. 2009. URL: https:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi.html"},{"key":"10_CR23","doi-asserted-by":"publisher","unstructured":"Bertrand Jeannet and Antoine Min\u00e9. \u201cApron: A Library of Numerical Abstract Domains for Static Analysis\u201d. In: CAV. 2009. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"10_CR24","doi-asserted-by":"publisher","unstructured":"Matthieu Journault, Antoine Min\u00e9, Rapha\u00ebl Monat, and Abdelraouf Ouadjaout. \u201cCombinations of Reusable Abstract Domains for a Multilingual Static Analyzer\u201d. In: VSTTE. 2019. https:\/\/doi.org\/10.1007\/978-3-030-41600-3_1","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Nikolai Kosmatov, Nicky Williams, Bernard Botella, and Muriel Roger. \u201cStructural Unit Testing as a Service with PathCrawler-online.com\u201d. In: SOSE. 2013. https:\/\/doi.org\/10.1109\/SOSE.2013.78","DOI":"10.1109\/SOSE.2013.78"},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Pierre Lermusiaux and Beno\u00eet Montagu. \u201cDetection of Uncaught Exceptions in Functional Programs by Abstract Interpretation\u201d. In: ESOP. 2024. https:\/\/doi.org\/10.1007\/978-3-031-57267-8_15","DOI":"10.1007\/978-3-031-57267-8_15"},{"key":"10_CR27","unstructured":"Pierre Lermusiaux and Beno\u00eet Montagu.Web Demo for the Salto Analyzer. 2025. URL: https:\/\/salto.gitlabpages.inria.fr\/demo\/salto.html"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Linghui Luo, Julian Dolby, and Eric Bodden. \u201cMagpieBridge: A General Approach to Integrating Static Analyses into IDEs and Editors (Tool Insights Paper)\u201d. In: ECOOP. 2019. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2019.21","DOI":"10.4230\/LIPICS.ECOOP.2019.21"},{"key":"10_CR29","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. \u201cInferring Sufficient Conditions with Backward Polyhedral Under-Approximations\u201d. In: NSAD@SAS. 2012. https:\/\/doi.org\/10.1016\/J.ENTCS.2012.09.009","DOI":"10.1016\/J.ENTCS.2012.09.009"},{"key":"10_CR30","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. \u201cRelational Abstract Domains for the Detection of Floating- Point Run-Time Errors\u2019. In: ESOP. 2004. https:\/\/doi.org\/10.1007\/978-3-540-24725-8_2","DOI":"10.1007\/978-3-540-24725-8_2"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"Antoine Min\u00e9. \u201cThe octagon abstract domain\u201d. In: High. Order Symb.Comput. 1 (2006). https:\/\/doi.org\/10.1007\/S10990-006-8609-1","DOI":"10.1007\/S10990-006-8609-1"},{"key":"10_CR32","unstructured":"Antoine Min\u00e9. Web Interface for Sufficient Condition Polyhedral Prototype Analyzer. 2012. URL: https:\/\/mine.perso.lip6.fr\/banal\/"},{"key":"10_CR33","unstructured":"Antoine Min\u00e9, Xavier Leroy, and Pascal Cuoq. Zarith: arithmetic and logical operations over arbitrary-precision integers. Version 1.14. July 2024. URL: https:\/\/github.com\/ocaml\/Zarith"},{"key":"10_CR34","unstructured":"Antoine Min\u00e9, Abdelraouf Ouadjaout, Matthieu Journault, Rapha\u00ebl Monat, Francesco Parolini, Marco Milanese, and J\u00e9r\u00f4me Boillot. Docker Containers for Each Mopsa Release. 2025. URL: https:\/\/gitlab.com\/mopsa\/mopsa-analyzer\/container_registry\/6390468"},{"key":"10_CR35","unstructured":"Alex Mojaki. sync-message. Version 0.0.12. Oct. 2023. URL: https:\/\/github.com\/alexmojaki\/sync-message"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Mats Van Molle, Bram Vandenbogaerde, and Coen De Roover. \u201cCross- Level Debugging for Static Analysers\u201d. In: SLE. 2023. https:\/\/doi.org\/10.1145\/3623476.3623512","DOI":"10.1145\/3623476.3623512"},{"key":"10_CR37","unstructured":"Rapha\u00ebl Monat. \u201cStatic Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries\u201d. PhD thesis. Sorbonne Universit\u00e9, France, 2021"},{"key":"10_CR38","unstructured":"Rapha\u00ebl Monat. Try-Mopsa. 2025. URL: https:\/\/try-mopsa.rmonat.fr"},{"key":"10_CR39","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17157478","author":"R Monat","year":"2025","unstructured":"Monat, R.: Try-Mopsa: Relational Static Analysis in Your Pocket (Artefact). Sept. (2025). https:\/\/doi.org\/10.5281\/zenodo.17157478","journal-title":"Sept."},{"key":"10_CR40","doi-asserted-by":"publisher","unstructured":"Rapha\u00ebl Monat, Abdelraouf Ouadjaout, and Antoine Min\u00e9. \u201cA Multilanguage Static Analysis of Python Programs with Native C Extensions\u201d. In: SAS. 2021. https:\/\/doi.org\/10.1007\/978-3-030-88806-0_16","DOI":"10.1007\/978-3-030-88806-0_16"},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Rapha\u00ebl Monat, Abdelraouf Ouadjaout, and Antoine Min\u00e9. \u201cEasing maintenance of academic static analyzers\u201d. In: Int. J. Softw. Tools Technol. Transf. 6 (2024). https:\/\/doi.org\/10.1007\/S10009-024-00770-1","DOI":"10.1007\/S10009-024-00770-1"},{"key":"10_CR42","doi-asserted-by":"publisher","unstructured":"Rapha\u00ebl Monat, Abdelraouf Ouadjaout, and Antoine Min\u00e9. \u201cMopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)\u201d. In: TACAS. 2023. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_37","DOI":"10.1007\/978-3-031-30820-8_37"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"Rapha\u00ebl Monat, Abdelraouf Ouadjaout, and Antoine Min\u00e9. \u201cStatic Type Analysis by Abstract Interpretation of Python Programs\u201d. In: ECOOP. 2020. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2020.17.","DOI":"10.4230\/LIPICS.ECOOP.2020.17."},{"key":"10_CR44","doi-asserted-by":"publisher","unstructured":"Beno\u00eet Montagu and Thomas P. Jensen. \u201cStable relations and abstract interpretation of higher-order programs\u201d. In: Proc. ACM Program. Lang. ICFP (2020). https:\/\/doi.org\/10.1145\/3409001","DOI":"10.1145\/3409001"},{"key":"10_CR45","doi-asserted-by":"publisher","unstructured":"Beno\u00eet Montagu and Thomas P. Jensen. \u201cTrace-based control-flow analysis\u201d. In: PLDI. 2021. https:\/\/doi.org\/10.1145\/3453483.3454057","DOI":"10.1145\/3453483.3454057"},{"key":"10_CR46","unstructured":"Jose F. Morales, Guillermo Garc\u00eda Pradales, and Manuel Hermenegildo. Ciao Prolog Playground. 2022. URL: https:\/\/ciao-lang.org\/playground\/"},{"key":"10_CR47","doi-asserted-by":"publisher","unstructured":"Luca Negrini, Vincenzo Arceri, Luca Olivieri, Agostino Cortesi, and Pietro Ferrara. \u201cTeaching Through Practice: Advanced Static Analysis with LiSA\u201d. In: FMTea. 2024. https:\/\/doi.org\/10.1007\/978-3-031-71379-8_3","DOI":"10.1007\/978-3-031-71379-8_3"},{"key":"10_CR48","unstructured":"OCamlPro. Ezjs_ace: bindings for the Ace editor. Version 0.1.1. Oct. 2020. url: https:\/\/github.com\/ocamlpro\/ezjs_ace"},{"key":"10_CR49","doi-asserted-by":"publisher","unstructured":"Abdelraouf Ouadjaout and Antoine Min\u00e9. \u201cA Library Modeling Language for the Static Analysis of C Programs\u201d. In: SAS. 2020. https:\/\/doi.org\/10.1007\/978-3-030-65474-0_11","DOI":"10.1007\/978-3-030-65474-0_11"},{"key":"10_CR50","unstructured":"Fran\u00e7ois Pottier and Yann R\u00e9gis-Gianas. Menhir: an LR(1) parser generator for OCaml. Version 20250903. Sept. 2025. URL: https:\/\/gitlab.inria.fr\/fpottier\/menhir"},{"key":"10_CR51","unstructured":"Fr\u00e9d\u00e9ric Recoules and S\u00e9bastien Bardin. BINSEC Tutorial at PLDI\u201925: Adapting Symbolic Execution for Binary-level Security. 2025. URL: https:\/\/binsec.github.io\/tutorial-pldi2025\/"},{"key":"10_CR52","unstructured":"The Ace Developers. Ace (Ajax.org Cloud9 Editor). Version 1.43.3. Sept. 2025. URL: https:\/\/github.com\/ajaxorg\/ace"},{"key":"10_CR53","unstructured":"The Playwright Development Team. Playwright: framework for Web Testing and Automation. Version 1.55.0. Sept. 8, 2025. URL: https:\/\/github.com\/microsoft\/playwright"},{"key":"10_CR54","doi-asserted-by":"publisher","unstructured":"Caterina Urban. \u201cFuncTion: An Abstract Domain Functor for Termination - (Competition Contribution)\u201d. In: TACAS. 2015. https:\/\/doi.org\/10.1007\/978-3-662-46681-0_46","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"10_CR55","unstructured":"Caterina Urban. Web Interface for FuncTion. 2015. URL: https:\/\/www.di.ens.fr\/~urban\/FuncTion.html"},{"key":"10_CR56","doi-asserted-by":"publisher","unstructured":"J\u00e9r\u00f4me Vouillon and Vincent Balat. \u201cFrom bytecode to JavaScript: the Js_of_ocaml compiler\u201d. In: Softw. Pract. Exp. 8 (2014). https:\/\/doi.org\/10.1002\/SPE.2187","DOI":"10.1002\/SPE.2187"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:54Z","timestamp":1768202514000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}