{"id":20807,"date":"2025-10-21T17:18:15","date_gmt":"2025-10-21T15:18:15","guid":{"rendered":"https:\/\/www.clearsy.com\/?p=20807"},"modified":"2025-10-21T17:18:15","modified_gmt":"2025-10-21T15:18:15","slug":"clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b","status":"publish","type":"post","link":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/","title":{"rendered":"CLEARSY works to improve the mathematical demonstration tools of Atelier B"},"content":{"rendered":"<p>As part of a project funded by the French National Research Agency (ANR), CLEARSY is collaborating with LORIA (Nancy), CRIL (Lens) and the University of Li\u00e8ge to improve the mathematical demonstration tools of Atelier B.<\/p>\n<p>When Atelier B is used to develop secure software, it produces mathematical proof obligations that must then be resolved.<\/p>\n<p>Atelier B&#8217;s demonstration tools (provers) already enable a large proportion of these to be resolved automatically.<\/p>\n<p>The project <em>\u201cEnhancing B Language Reasoners with SAT and SMT Techniques\u201d<\/em> aims to improve the efficiency of these demonstrators.<\/p>\n<p>The initial results are already conclusive!<\/p>\n<p>On a test bench of 681,285 proof obligations, techniques based on SAT-type consistency verification tools and SMT-type consistency checking tools have enabled us to increase the number of automatically proven proof obligations from <strong>74% to 87%.<\/strong><\/p>\n<p><strong><span>TARGET:<\/span> Over 90% by the end of the project in March 2027!<\/strong><\/p>\n","protected":false},"excerpt":{"rendered":"<p>As part of a project funded by the French National Research Agency (ANR), CLEARSY is collaborating with LORIA (Nancy), CRIL [&hellip;]<\/p>\n","protected":false},"author":23,"featured_media":20804,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_acf_changed":false,"footnotes":""},"categories":[1541,685,1550,1551,686],"tags":[],"class_list":["post-20807","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-computer-science","category-the-offers","category-rd-2-en","category-surete-de-fonctionnement-en","category-the-tools"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.3 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"As part of a project funded by the French National Research Agency (ANR), CLEARSY is collaborating with LORIA (Nancy), CRIL [&hellip;]\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:published_time\" content=\"2025-10-21T15:18:15+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg\" \/>\n\t<meta property=\"og:image:width\" content=\"1700\" \/>\n\t<meta property=\"og:image:height\" content=\"650\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"author\" content=\"Elodie SENOUCI-TANI\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"Elodie SENOUCI-TANI\" \/>\n\t<meta name=\"twitter:label2\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data2\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/\"},\"author\":{\"name\":\"Elodie SENOUCI-TANI\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/person\\\/814317cfd25d55208a01568fae4dc689\"},\"headline\":\"CLEARSY works to improve the mathematical demonstration tools of Atelier B\",\"datePublished\":\"2025-10-21T15:18:15+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/\"},\"wordCount\":151,\"publisher\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2025\\\/10\\\/BLASST-US-web-1.jpeg\",\"articleSection\":[\"Computer science\",\"Offers\",\"R&amp;D\",\"S\u00fbret\u00e9 de fonctionnement\",\"Tools\"],\"inLanguage\":\"en-US\"},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/\",\"name\":\"CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2025\\\/10\\\/BLASST-US-web-1.jpeg\",\"datePublished\":\"2025-10-21T15:18:15+00:00\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#primaryimage\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2025\\\/10\\\/BLASST-US-web-1.jpeg\",\"contentUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2025\\\/10\\\/BLASST-US-web-1.jpeg\",\"width\":1700,\"height\":650,\"caption\":\"CLEARSY works to improve the mathematical demonstration tools of Atelier B\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/rd-2-en\\\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"CLEARSY works to improve the mathematical demonstration tools of Atelier B\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#website\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\",\"name\":\"CLEARSY\",\"description\":\"Safety Solutions Designer\",\"publisher\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"},{\"@type\":\"Organization\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#organization\",\"name\":\"CLEARSY\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/logo\\\/image\\\/\",\"url\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/04\\\/logo-clearsy.svg\",\"contentUrl\":\"https:\\\/\\\/www.clearsy.com\\\/wp-content\\\/uploads\\\/2020\\\/04\\\/logo-clearsy.svg\",\"width\":652,\"height\":163,\"caption\":\"CLEARSY\"},\"image\":{\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/logo\\\/image\\\/\"}},{\"@type\":\"Person\",\"@id\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/#\\\/schema\\\/person\\\/814317cfd25d55208a01568fae4dc689\",\"name\":\"Elodie SENOUCI-TANI\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g\",\"caption\":\"Elodie SENOUCI-TANI\"},\"url\":\"https:\\\/\\\/www.clearsy.com\\\/en\\\/author\\\/esenouci\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/","og_locale":"en_US","og_type":"article","og_title":"CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY","og_description":"As part of a project funded by the French National Research Agency (ANR), CLEARSY is collaborating with LORIA (Nancy), CRIL [&hellip;]","og_url":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/","og_site_name":"CLEARSY","article_published_time":"2025-10-21T15:18:15+00:00","og_image":[{"width":1700,"height":650,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg","type":"image\/jpeg"}],"author":"Elodie SENOUCI-TANI","twitter_card":"summary_large_image","twitter_misc":{"Written by":"Elodie SENOUCI-TANI","Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#article","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/"},"author":{"name":"Elodie SENOUCI-TANI","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/person\/814317cfd25d55208a01568fae4dc689"},"headline":"CLEARSY works to improve the mathematical demonstration tools of Atelier B","datePublished":"2025-10-21T15:18:15+00:00","mainEntityOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/"},"wordCount":151,"publisher":{"@id":"https:\/\/www.clearsy.com\/en\/#organization"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg","articleSection":["Computer science","Offers","R&amp;D","S\u00fbret\u00e9 de fonctionnement","Tools"],"inLanguage":"en-US"},{"@type":"WebPage","@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/","url":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/","name":"CLEARSY works to improve the mathematical demonstration tools of Atelier B - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg","datePublished":"2025-10-21T15:18:15+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2025\/10\/BLASST-US-web-1.jpeg","width":1700,"height":650,"caption":"CLEARSY works to improve the mathematical demonstration tools of Atelier B"},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/rd-2-en\/clearsy-works-to-improve-the-mathematical-demonstration-tools-of-atelier-b\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"CLEARSY works to improve the mathematical demonstration tools of Atelier B"}]},{"@type":"WebSite","@id":"https:\/\/www.clearsy.com\/en\/#website","url":"https:\/\/www.clearsy.com\/en\/","name":"CLEARSY","description":"Safety Solutions Designer","publisher":{"@id":"https:\/\/www.clearsy.com\/en\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.clearsy.com\/en\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"},{"@type":"Organization","@id":"https:\/\/www.clearsy.com\/en\/#organization","name":"CLEARSY","url":"https:\/\/www.clearsy.com\/en\/","logo":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/logo\/image\/","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/04\/logo-clearsy.svg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2020\/04\/logo-clearsy.svg","width":652,"height":163,"caption":"CLEARSY"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/logo\/image\/"}},{"@type":"Person","@id":"https:\/\/www.clearsy.com\/en\/#\/schema\/person\/814317cfd25d55208a01568fae4dc689","name":"Elodie SENOUCI-TANI","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/secure.gravatar.com\/avatar\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/501a9cdd7eeba9e36ae784c53b209c3629e3e856bc8e66cea6ad8f7f8ebe97ba?s=96&d=mm&r=g","caption":"Elodie SENOUCI-TANI"},"url":"https:\/\/www.clearsy.com\/en\/author\/esenouci\/"}]}},"_links":{"self":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/20807","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/users\/23"}],"replies":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/comments?post=20807"}],"version-history":[{"count":3,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/20807\/revisions"}],"predecessor-version":[{"id":20810,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/posts\/20807\/revisions\/20810"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/20804"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=20807"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/categories?post=20807"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/tags?post=20807"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}