CINXE.COM

<!DOCTYPE html> <html lang="en"> <head> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> <meta charset="utf-8"> <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no"> <meta http-equiv="X-UA-Compatible" content="IE=edge"> <title> Diego Marmsoler </title> <meta name="author" content="Diego Marmsoler"> <meta name="description" content="Software Engineering and Formal Methods. "> <meta name="keywords" content="diego-marmsoler, formal-methods"> <link rel="stylesheet" href="/assets/css/bootstrap.min.css?a4b3f509e79c54a512b890d73235ef04"> <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/mdbootstrap@4.20.0/css/mdb.min.css" integrity="sha256-jpjYvU3G3N6nrrBwXJoVEYI/0zw8htfFnhT9ljN3JJw=" crossorigin="anonymous"> <link defer rel="stylesheet" href="/assets/css/academicons.min.css?f0b7046b84e425c55f3463ac249818f5"> <link defer rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=Roboto:300,400,500,700|Roboto+Slab:100,300,400,500,700|Material+Icons&display=swap"> <link defer rel="stylesheet" href="/assets/css/jekyll-pygments-themes-github.css?591dab5a4e56573bf4ef7fd332894c99" media="" id="highlight_theme_light"> <link rel="shortcut icon" href="/assets/img/logo.png?c01ff7daabbe3f79487c4a217246219f"> <link rel="stylesheet" href="/assets/css/main.css?d41d8cd98f00b204e9800998ecf8427e"> <link rel="canonical" href="https://dmarmsoler.github.io/"> <script src="/assets/js/theme.js?9a0c749ec5240d9cda97bc72359a72c0"></script> <link defer rel="stylesheet" href="/assets/css/jekyll-pygments-themes-native.css?5847e5ed4a4568527aa6cfab446049ca" media="none" id="highlight_theme_dark"> <script>initTheme();</script> </head> <body class="fixed-top-nav "> <header> <nav id="navbar" class="navbar navbar-light navbar-expand-sm fixed-top" role="navigation"> <div class="container"> <button class="navbar-toggler collapsed ml-auto" type="button" data-toggle="collapse" data-target="#navbarNav" aria-controls="navbarNav" aria-expanded="false" aria-label="Toggle navigation"> <span class="sr-only">Toggle navigation</span> <span class="icon-bar top-bar"></span> <span class="icon-bar middle-bar"></span> <span class="icon-bar bottom-bar"></span> </button> <div class="collapse navbar-collapse text-right" id="navbarNav"> <ul class="navbar-nav ml-auto flex-nowrap"> <li class="nav-item active"> <a class="nav-link" href="/">about <span class="sr-only">(current)</span> </a> </li> <li class="nav-item "> <a class="nav-link" href="/publications/">publications </a> </li> <li class="nav-item "> <a class="nav-link" href="/projects/">projects </a> </li> <li class="nav-item "> <a class="nav-link" href="/cv/">cv </a> </li> <li class="nav-item "> <a class="nav-link" href="/teaching/">teaching </a> </li> <li class="nav-item "> <a class="nav-link" href="/people/">people </a> </li> <li class="nav-item"> <button id="search-toggle" title="Search" onclick="openSearchModal()"> <span class="nav-link">ctrl k <i class="ti ti-search"></i></span> </button> </li> <li class="toggle-container"> <button id="light-toggle" title="Change theme"> <i class="ti ti-sun-moon" id="light-toggle-system"></i> <i class="ti ti-moon-filled" id="light-toggle-dark"></i> <i class="ti ti-sun-filled" id="light-toggle-light"></i> </button> </li> </ul> </div> </div> </nav> <progress id="progress" value="0"> <div class="progress-container"> <span class="progress-bar"></span> </div> </progress> </header> <div class="container mt-5" role="main"> <div class="post"> <header class="post-header"> <h1 class="post-title"> <span class="font-weight-bold">Diego</span> Marmsoler </h1> <p class="desc">Software Engineering and Formal Methods</p> </header> <article> <div class="profile float-right"> <figure> <picture> <source class="responsive-img-srcset" srcset="/assets/img/diego_marmsoler.jpg" sizes="(min-width: 930px) 270.0px, (min-width: 576px) 30vw, 95vw"> <img src="/assets/img/diego_marmsoler.jpg?d3fadada0dd68f7e87449bbe7e2c905d" class="img-fluid z-depth-1 rounded" width="100%" height="auto" alt="diego_marmsoler.jpg" loading="eager" onerror="this.onerror=null; $('.responsive-img-srcset').remove();"> </source></picture> </figure> <div class="more-info"> <p><a href="https://maps.app.goo.gl/94F5SaneEcvvyBqt5" rel="external nofollow noopener" target="_blank">Innovation Centre 1</a> Mb</p> <p>Rennes Dr</p> <p>Exeter, Devon, EX4 4RN</p> </div> </div> <div class="clearfix"> <p>I am a lecturer (E&R) in the <a href="https://computerscience.exeter.ac.uk/research/cyber-security/" rel="external nofollow noopener" target="_blank">Cyber Security group</a> at the <a href="https://www.exeter.ac.uk/" rel="external nofollow noopener" target="_blank">University of Exeter</a>. Before, I was a postdoctoral researcher at the Software and Systems Engineering group of Prof. Manfred Broy at the Technical University of Munich. I obtained a B.Sc. from the Free University of Bozen-Bolzano and an M.Sc. from the TU München, LMU, and Augsburg University. I received my Ph.D. in Computer Science from the Technical University of Munich in 2019.</p> <p>In general, my research focuses on the formal specification and verification of distributed, component-based systems. Specifically, I am working on the integration of automatic (Model Checking, Runtime Verification) and semi-automatic (Interactive Theorem Proving) techniques for the verification of such systems. Recently, I started to apply these techniques for the verification of dynamically adapting architectures and architectures in the area of Blockchain.</p> </div> <h2> <a href="/news/" style="color: inherit">news</a> </h2> <div class="news"> <div class="table-responsive" style="max-height: 60vw"> <table class="table table-sm table-borderless"> <tr> <th scope="row" style="width: 20%">Oct 17, 2024</th> <td> <a class="news-title" href="/news/augusto25/">Augusto Sampaio visiting our group</a> </td> </tr> <tr> <th scope="row" style="width: 20%">Oct 15, 2024</th> <td> <a class="news-title" href="/news/fac/">New FAC paper</a> </td> </tr> <tr> <th scope="row" style="width: 20%">Oct 10, 2024</th> <td> <a class="news-title" href="/news/fmbc25/">FMBC 25 @ ETAPS 2025</a> </td> </tr> <tr> <th scope="row" style="width: 20%">Aug 31, 2024</th> <td> <a class="news-title" href="/news/ictac24/">Paper accepted for ICTAC24</a> </td> </tr> <tr> <th scope="row" style="width: 20%">Aug 22, 2024</th> <td> <a class="news-title" href="/news/sefm24/">Paper accepted for SEFM24</a> </td> </tr> </table> </div> </div> <h2> <a href="/publications/" style="color: inherit">selected publications</a> </h2> <div class="publications"> <ol class="bibliography"> <li> <div class="row"> <div class="col col-sm-2 abbr"> <abbr class="badge rounded w-100" style="background-color:#c32b72"> <a href="https://dl.acm.org/journal/fac" rel="external nofollow noopener" target="_blank">FAC</a> </abbr> </div> <div id="Marmsoler2024b" class="col-sm-8"> <div class="title">Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL</div> <div class="author"> <em>Diego Marmsoler</em>, and Achim D. Brucker </div> <div class="periodical"> <em>Formal Aspects Computing</em>, Oct 2024 </div> <div class="periodical"> </div> <div class="links"> <a class="abstract btn btn-sm z-depth-0" role="button">Abs</a> <a class="bibtex btn btn-sm z-depth-0" role="button">Bib</a> <a href="https://dl.acm.org/doi/epdf/10.1145/3700601" class="btn btn-sm z-depth-0" role="button" rel="external nofollow noopener" target="_blank">HTML</a> <a href="https://dl.acm.org/doi/pdf/10.1145/3700601" class="btn btn-sm z-depth-0" role="button" rel="external nofollow noopener" target="_blank">PDF</a> </div> <div class="abstract hidden"> <p>Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars’ worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts. This paper addresses the issue of smart contract vulnerabilities by introducing an executable denotational semantics for Solidity within the Isabelle/HOL interactive theorem prover. This formal semantics serves as the basis for an interactive program verification environment for Solidity smart contracts. To evaluate our semantics, we integrate grammar-based fuzzing with symbolic execution to automatically test it against the Solidity reference implementation. The paper concludes by showcasing the formal verification of Solidity programs, exemplified through the verification of a basic Solidity token.</p> </div> <div class="bibtex hidden"> <figure class="highlight"><pre><code class="language-bibtex" data-lang="bibtex"><span class="nc">@article</span><span class="p">{</span><span class="nl">Marmsoler2024b</span><span class="p">,</span> <span class="na">author</span> <span class="p">=</span> <span class="s">{Marmsoler, Diego and Brucker, Achim D.}</span><span class="p">,</span> <span class="na">title</span> <span class="p">=</span> <span class="s">{Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL}</span><span class="p">,</span> <span class="na">year</span> <span class="p">=</span> <span class="s">{2024}</span><span class="p">,</span> <span class="na">publisher</span> <span class="p">=</span> <span class="s">{Association for Computing Machinery}</span><span class="p">,</span> <span class="na">address</span> <span class="p">=</span> <span class="s">{New York, NY, USA}</span><span class="p">,</span> <span class="na">issn</span> <span class="p">=</span> <span class="s">{0934-5043}</span><span class="p">,</span> <span class="na">url</span> <span class="p">=</span> <span class="s">{https://doi.org/10.1145/3700601}</span><span class="p">,</span> <span class="na">doi</span> <span class="p">=</span> <span class="s">{10.1145/3700601}</span><span class="p">,</span> <span class="na">journal</span> <span class="p">=</span> <span class="s">{Formal Aspects Computing}</span><span class="p">,</span> <span class="na">month</span> <span class="p">=</span> <span class="nv">oct</span><span class="p">,</span> <span class="na">keywords</span> <span class="p">=</span> <span class="s">{Solidity, Denotational Semantics, Isabelle/HOL}</span><span class="p">,</span> <span class="p">}</span></code></pre></figure> </div> </div> </div> </li> <li> <div class="row"> <div class="col col-sm-2 abbr"> <abbr class="badge rounded w-100" style="background-color:#c32b72"> <a href="https://www.sciencedirect.com/journal/science-of-computer-programming" rel="external nofollow noopener" target="_blank">SCP</a> </abbr> </div> <div id="Marmsoler2019b" class="col-sm-8"> <div class="title">A Calculus for Dynamic Architectures</div> <div class="author"> <em>Diego Marmsoler</em> </div> <div class="periodical"> <em>Science of Computer Programming</em>, Oct 2019 </div> <div class="periodical"> </div> <div class="links"> <a class="abstract btn btn-sm z-depth-0" role="button">Abs</a> <a href="/assets/pdf/marmsoler_19_calculus_dynamic_architectures" class="btn btn-sm z-depth-0" role="button">PDF</a> </div> <div class="abstract hidden"> <p>With the emergence of mobile and adaptive computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections between them may change over time. Dynamic architectures are usually specified in terms of two separate specifications: a specification of component behavior and a specification of component activation and reconfiguration. To verify them, both specifications are first interpreted over a common model for dynamic architectures and verified against a property specified over the same model. Interpreting the specifications over the model, however, introduce repetitive proof steps, which increase the length of proofs, and thus the effort to develop and maintain them. To address this problem, we developed a calculus for dynamic architectures providing rules to reason about component behavior in a dynamic environment. We proved soundness and relative completeness of the rules, implemented them in the interactive theorem prover Isabelle, and mechanized the corresponding soundness proofs. The calculus can be used to support the abstract verification of dynamic architectures in Isabelle. This is demonstrated by means of a running example and evaluated in terms of four case studies. Our results suggest that the calculus has the potential to reduce the length of proofs for the verification of dynamic architectures, thus reducing the effort to develop and maintain verification results.</p> </div> </div> </div> </li> <li> <div class="row"> <div class="col col-sm-2 abbr"> <abbr class="badge rounded w-100" style="background-color:#c32b72"> <a href="https://dl.acm.org/journal/fac" rel="external nofollow noopener" target="_blank">FAC</a> </abbr> </div> <div id="Marmsoler2019c" class="col-sm-8"> <div class="title">Interactive Verification of Architectural Design Patterns in FACTum</div> <div class="author"> <em>Diego Marmsoler</em>, and Habtom Kahsay Gidey </div> <div class="periodical"> <em>Formal Aspects Computing</em>, Oct 2019 </div> <div class="periodical"> </div> <div class="links"> <a class="abstract btn btn-sm z-depth-0" role="button">Abs</a> <a href="/assets/pdf/marmsoler_19_factum.pdf" class="btn btn-sm z-depth-0" role="button">PDF</a> </div> <div class="abstract hidden"> <p>Architectural design patterns (ADPs) are architectural solutions to common architectural design problems. They are an important concept in software architectures used for the design and analysis of architectures. An ADP usually constrains the design of an architecture and, in turn, guarantees some desired properties for architectures implementing it. Sometimes, however, the constraints imposed by an ADP do not lead to the claimed guarantee. Thus, applying such patterns for the design of architectures might result in architectures which do not fulfill their intended requirements. To address this problem, we propose an approach for the verification of ADPs, based on interactive theorem proving. To this end, we introduce a model for dynamic architectures and a language for the specification of ADPs over this model. Moreover, we propose a framework for the interactive verification of such specifications based on Isabelle/HOL. In addition we describe an algorithm to map a specifi cation to a corresponding Isabelle/HOL theory over our framework. To evaluate the approach, we implement it in Eclipse/EMF and use it for the verification of four ADPs: variants of the Singleton, the Publisher-Subscriber, the Blackboard pattern, and a pattern for Blockchain architectures. With our approach we complement traditional approaches for the verification of architectures, which are usually based on automatic verification techniques such as model checking.</p> </div> </div> </div> </li> <li> <div class="row"> <div class="col col-sm-2 abbr"> <abbr class="badge rounded w-100" style="background-color:#196ca3"> <a href="https://sefm-conference.github.io/" rel="external nofollow noopener" target="_blank">SEFM</a> </abbr> </div> <div id="Marmsoler2023" class="col-sm-8"> <div class="title">SSCalc: A Calculus for Solidity Smart Contracts</div> <div class="author"> <em>Diego Marmsoler</em>, and Billy Thornton </div> <div class="periodical"> <em>In Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings</em>, Oct 2023 </div> <div class="periodical"> </div> <div class="links"> <a class="abstract btn btn-sm z-depth-0" role="button">Abs</a> <a href="/assets/pdf/marmsoler_23_sscalc.pdf" class="btn btn-sm z-depth-0" role="button">PDF</a> </div> <div class="abstract hidden"> <p>Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we describe a Verification Condition Generator to automate the use of the calculus. Our approach can be used to verify the functional correctness of Solidity smart contracts. To demonstrate this, we use it to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.</p> </div> </div> </div> </li> </ol> </div> <div class="social"> <div class="contact-icons"> <a href="mailto:%64.%6D%61%72%6D%73%6F%6C%65%72@%65%78%65%74%65%72.%61%63.%75%6B" title="email"><i class="fa-solid fa-envelope"></i></a> <a href="https://orcid.org/https://orcid.org/0000-0003-2859-7673" title="ORCID" rel="external nofollow noopener" target="_blank"><i class="ai ai-orcid"></i></a> <a href="https://scholar.google.com/citations?user=hw9lm9MAAAAJ" title="Google Scholar" rel="external nofollow noopener" target="_blank"><i class="ai ai-google-scholar"></i></a> <a href="https://github.com/dmarmsoler" title="GitHub" rel="external nofollow noopener" target="_blank"><i class="fa-brands fa-github"></i></a> <a href="https://twitter.com/DiegoMarmsoler" title="X" rel="external nofollow noopener" target="_blank"><i class="fa-brands fa-x-twitter"></i></a> <a href="/feed.xml" title="RSS Feed"><i class="fa-solid fa-square-rss"></i></a> </div> <div class="contact-note"></div> </div> </article> </div> </div> <footer class="fixed-bottom" role="contentinfo"> <div class="container mt-0"> © Copyright 2024 Diego Marmsoler. Powered by <a href="https://jekyllrb.com/" target="_blank" rel="external nofollow noopener">Jekyll</a> with <a href="https://github.com/alshedivat/al-folio" rel="external nofollow noopener" target="_blank">al-folio</a> theme. Hosted by <a href="https://pages.github.com/" target="_blank" rel="external nofollow noopener">GitHub Pages</a>. </div> </footer> <script src="https://cdn.jsdelivr.net/npm/jquery@3.6.0/dist/jquery.min.js" integrity="sha256-/xUj+3OJU5yExlq6GSYGSHk7tPXikynS7ogEvDej/m4=" crossorigin="anonymous"></script> <script src="/assets/js/bootstrap.bundle.min.js"></script> <script src="https://cdn.jsdelivr.net/npm/mdbootstrap@4.20.0/js/mdb.min.js" integrity="sha256-NdbiivsvWt7VYCt6hYNT3h/th9vSTL4EDWeGs5SN3DA=" crossorigin="anonymous"></script> <script defer src="https://cdn.jsdelivr.net/npm/masonry-layout@4.2.2/dist/masonry.pkgd.min.js" integrity="sha256-Nn1q/fx0H7SNLZMQ5Hw5JLaTRZp0yILA/FRexe19VdI=" crossorigin="anonymous"></script> <script defer src="https://cdn.jsdelivr.net/npm/imagesloaded@5.0.0/imagesloaded.pkgd.min.js" integrity="sha256-htrLFfZJ6v5udOG+3kNLINIKh2gvoKqwEhHYfTTMICc=" crossorigin="anonymous"></script> <script defer src="/assets/js/masonry.js" type="text/javascript"></script> <script defer src="https://cdn.jsdelivr.net/npm/medium-zoom@1.1.0/dist/medium-zoom.min.js" integrity="sha256-ZgMyDAIYDYGxbcpJcfUnYwNevG/xi9OHKaR/8GK+jWc=" crossorigin="anonymous"></script> <script defer src="/assets/js/zoom.js?85ddb88934d28b74e78031fd54cf8308"></script> <script src="/assets/js/no_defer.js?2781658a0a2b13ed609542042a859126"></script> <script defer src="/assets/js/common.js?e0514a05c5c95ac1a93a8dfd5249b92e"></script> <script defer src="/assets/js/copy_code.js?12775fdf7f95e901d7119054556e495f" type="text/javascript"></script> <script defer src="/assets/js/jupyter_new_tab.js?d9f17b6adc2311cbabd747f4538bb15f"></script> <script type="text/javascript">window.MathJax={tex:{tags:"ams"}};</script> <script defer type="text/javascript" id="MathJax-script" src="https://cdn.jsdelivr.net/npm/mathjax@3.2.2/es5/tex-mml-chtml.js" integrity="sha256-MASABpB4tYktI2Oitl4t+78w/lyA+D7b/s9GEP0JOGI=" crossorigin="anonymous"></script> <script defer src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6" crossorigin="anonymous"></script> <script type="text/javascript">function progressBarSetup(){"max"in document.createElement("progress")?(initializeProgressElement(),$(document).on("scroll",function(){progressBar.attr({value:getCurrentScrollPosition()})}),$(window).on("resize",initializeProgressElement)):(resizeProgressBar(),$(document).on("scroll",resizeProgressBar),$(window).on("resize",resizeProgressBar))}function getCurrentScrollPosition(){return $(window).scrollTop()}function initializeProgressElement(){let e=$("#navbar").outerHeight(!0);$("body").css({"padding-top":e}),$("progress-container").css({"padding-top":e}),progressBar.css({top:e}),progressBar.attr({max:getDistanceToScroll(),value:getCurrentScrollPosition()})}function getDistanceToScroll(){return $(document).height()-$(window).height()}function resizeProgressBar(){progressBar.css({width:getWidthPercentage()+"%"})}function getWidthPercentage(){return getCurrentScrollPosition()/getDistanceToScroll()*100}const progressBar=$("#progress");window.onload=function(){setTimeout(progressBarSetup,50)};</script> <script src="/assets/js/vanilla-back-to-top.min.js?f40d453793ff4f64e238e420181a1d17"></script> <script>addBackToTop();</script> <script type="module" src="/assets/js/search/ninja-keys.min.js?a3446f084dcaecc5f75aa1757d087dcf"></script> <ninja-keys hidebreadcrumbs noautoloadmdicons placeholder="Type to start searching"></ninja-keys> <script>let searchTheme=determineComputedTheme();const ninjaKeys=document.querySelector("ninja-keys");"dark"===searchTheme?ninjaKeys.classList.add("dark"):ninjaKeys.classList.remove("dark");const openSearchModal=()=>{const e=$("#navbarNav");e.hasClass("show")&&e.collapse("hide"),ninjaKeys.open()};</script> <script>const ninja=document.querySelector("ninja-keys");ninja.data=[{id:"nav-about",title:"about",section:"Navigation",handler:()=>{window.location.href="/"}},{id:"nav-publications",title:"publications",description:"",section:"Navigation",handler:()=>{window.location.href="/publications/"}},{id:"nav-projects",title:"projects",description:"",section:"Navigation",handler:()=>{window.location.href="/projects/"}},{id:"nav-cv",title:"cv",description:"This is a description of the page. You can modify it in '_pages/cv.md'. You can also change or remove the top pdf download button.",section:"Navigation",handler:()=>{window.location.href="/cv/"}},{id:"nav-teaching",title:"teaching",description:"Modules I currently teach or taught in the past",section:"Navigation",handler:()=>{window.location.href="/teaching/"}},{id:"nav-people",title:"people",description:"members of the lab or group",section:"Navigation",handler:()=>{window.location.href="/people/"}},{id:"post-a-post-with-tabs",title:"a post with tabs",description:"this is what included tabs in a post could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/tabs/"}},{id:"post-a-post-with-typograms",title:"a post with typograms",description:"this is what included typograms code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/typograms/"}},{id:"post-a-post-that-can-be-cited",title:"a post that can be cited",description:"this is what a post that can be cited looks like",section:"Posts",handler:()=>{window.location.href="/blog/2024/post-citation/"}},{id:"post-a-post-with-pseudo-code",title:"a post with pseudo code",description:"this is what included pseudo code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/pseudocode/"}},{id:"post-a-post-with-code-diff",title:"a post with code diff",description:"this is how you can display code diffs",section:"Posts",handler:()=>{window.location.href="/blog/2024/code-diff/"}},{id:"post-a-post-with-advanced-image-components",title:"a post with advanced image components",description:"this is what advanced image components could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/advanced-images/"}},{id:"post-a-post-with-vega-lite",title:"a post with vega lite",description:"this is what included vega lite code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/vega-lite/"}},{id:"post-a-post-with-geojson",title:"a post with geojson",description:"this is what included geojson code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/geojson-map/"}},{id:"post-a-post-with-echarts",title:"a post with echarts",description:"this is what included echarts code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/echarts/"}},{id:"post-a-post-with-chart-js",title:"a post with chart.js",description:"this is what included chart.js code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2024/chartjs/"}},{id:"post-a-post-with-tikzjax",title:"a post with TikZJax",description:"this is what included TikZ code could look like",section:"Posts",handler:()=>{window.location.href="/blog/2023/tikzjax/"}},{id:"post-a-post-with-bibliography",title:"a post with bibliography",description:"an example of a blog post with bibliography",section:"Posts",handler:()=>{window.location.href="/blog/2023/post-bibliography/"}},{id:"post-a-post-with-jupyter-notebook",title:"a post with jupyter notebook",description:"an example of a blog post with jupyter notebook",section:"Posts",handler:()=>{window.location.href="/blog/2023/jupyter-notebook/"}},{id:"post-a-post-with-custom-blockquotes",title:"a post with custom blockquotes",description:"an example of a blog post with custom blockquotes",section:"Posts",handler:()=>{window.location.href="/blog/2023/custom-blockquotes/"}},{id:"post-a-post-with-table-of-contents-on-a-sidebar",title:"a post with table of contents on a sidebar",description:"an example of a blog post with table of contents on a sidebar",section:"Posts",handler:()=>{window.location.href="/blog/2023/sidebar-table-of-contents/"}},{id:"post-a-post-with-audios",title:"a post with audios",description:"this is what included audios could look like",section:"Posts",handler:()=>{window.location.href="/blog/2023/audios/"}},{id:"post-a-post-with-videos",title:"a post with videos",description:"this is what included videos could look like",section:"Posts",handler:()=>{window.location.href="/blog/2023/videos/"}},{id:"post-displaying-beautiful-tables-with-bootstrap-tables",title:"displaying beautiful tables with Bootstrap Tables",description:"an example of how to use Bootstrap Tables",section:"Posts",handler:()=>{window.location.href="/blog/2023/tables/"}},{id:"post-a-post-with-table-of-contents",title:"a post with table of contents",description:"an example of a blog post with table of contents",section:"Posts",handler:()=>{window.location.href="/blog/2023/table-of-contents/"}},{id:"post-a-post-with-giscus-comments",title:"a post with giscus comments",description:"an example of a blog post with giscus comments",section:"Posts",handler:()=>{window.location.href="/blog/2022/giscus-comments/"}},{id:"post-a-post-with-redirect",title:"a post with redirect",description:"you can also redirect to assets like pdf",section:"Posts",handler:()=>{window.location.href="/assets/pdf/example_pdf.pdf"}},{id:"post-a-post-with-diagrams",title:"a post with diagrams",description:"an example of a blog post with diagrams",section:"Posts",handler:()=>{window.location.href="/blog/2021/diagrams/"}},{id:"post-a-distill-style-blog-post",title:"a distill-style blog post",description:"an example of a distill-style blog post and main elements",section:"Posts",handler:()=>{window.location.href="/blog/2021/distill/"}},{id:"post-a-post-with-twitter",title:"a post with twitter",description:"an example of a blog post with twitter",section:"Posts",handler:()=>{window.location.href="/blog/2020/twitter/"}},{id:"post-a-post-with-disqus-comments",title:"a post with disqus comments",description:"an example of a blog post with disqus comments",section:"Posts",handler:()=>{window.location.href="/blog/2015/disqus-comments/"}},{id:"post-a-post-with-math",title:"a post with math",description:"an example of a blog post with some math",section:"Posts",handler:()=>{window.location.href="/blog/2015/math/"}},{id:"post-a-post-with-code",title:"a post with code",description:"an example of a blog post with some code",section:"Posts",handler:()=>{window.location.href="/blog/2015/code/"}},{id:"post-a-post-with-images",title:"a post with images",description:"this is what included images could look like",section:"Posts",handler:()=>{window.location.href="/blog/2015/images/"}},{id:"post-a-post-with-formatting-and-links",title:"a post with formatting and links",description:"march & april, looking forward to summer",section:"Posts",handler:()=>{window.location.href="/blog/2015/formatting-and-links/"}},{id:"news-paper-accepted-for-sefm24",title:"Paper accepted for SEFM24",description:"",section:"News",handler:()=>{window.location.href="/news/sefm24/"}},{id:"news-paper-accepted-for-ictac24",title:"Paper accepted for ICTAC24",description:"",section:"News",handler:()=>{window.location.href="/news/ictac24/"}},{id:"news-fmbc-25-etaps-2025",title:"FMBC 25 @ ETAPS 2025",description:"",section:"News",handler:()=>{window.location.href="/news/fmbc25/"}},{id:"news-new-fac-paper",title:"New FAC paper",description:"",section:"News",handler:()=>{window.location.href="/news/fac/"}},{id:"news-augusto-sampaio-visiting-our-group",title:"Augusto Sampaio visiting our group",description:"",section:"News",handler:()=>{window.location.href="/news/augusto25/"}},{id:"projects-factum",title:"FACTum",description:"A framework for the verification of component-based systems",section:"Projects",handler:()=>{window.location.href="/projects/factum/"}},{id:"projects-isabelle-solidity",title:"Isabelle/Solidity",description:"A framework for the verification of Solidity smart contracts in Isabelle",section:"Projects",handler:()=>{window.location.href="/projects/isabelle_solidity/"}},{id:"socials-email",title:"Send email",section:"Socials",handler:()=>{window.open("mailto:%64.%6D%61%72%6D%73%6F%6C%65%72@%65%78%65%74%65%72.%61%63.%75%6B","_blank")}},{id:"socials-orcid",title:"ORCID",section:"Socials",handler:()=>{window.open("https://orcid.org/https://orcid.org/0000-0003-2859-7673","_blank")}},{id:"socials-google-scholar",title:"Google Scholar",section:"Socials",handler:()=>{window.open("https://scholar.google.com/citations?user=hw9lm9MAAAAJ","_blank")}},{id:"socials-github",title:"GitHub",section:"Socials",handler:()=>{window.open("https://github.com/dmarmsoler","_blank")}},{id:"socials-x",title:"X",description:"Twitter",section:"Socials",handler:()=>{window.open("https://twitter.com/DiegoMarmsoler","_blank")}},{id:"socials-rss",title:"RSS Feed",section:"Socials",handler:()=>{window.open("/feed.xml","_blank")}},{id:"light-theme",title:"Change theme to light",description:"Change the theme of the site to Light",section:"Theme",handler:()=>{setThemeSetting("light")}},{id:"dark-theme",title:"Change theme to dark",description:"Change the theme of the site to Dark",section:"Theme",handler:()=>{setThemeSetting("dark")}},{id:"system-theme",title:"Use system default theme",description:"Change the theme of the site to System Default",section:"Theme",handler:()=>{setThemeSetting("system")}}];</script> <script src="/assets/js/shortcut-key.js?6f508d74becd347268a7f822bca7309d"></script> </body> </html>