{"id":17829,"date":"2021-09-07T14:41:37","date_gmt":"2021-09-07T12:41:37","guid":{"rendered":"https:\/\/www.clearsy.com\/?post_type=recherche&#038;p=17829"},"modified":"2021-09-07T14:44:50","modified_gmt":"2021-09-07T12:44:50","slug":"blasst","status":"publish","type":"recherche","link":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/","title":{"rendered":"BLASST"},"content":{"rendered":"<p><a href=\"https:\/\/anr.fr\/\">ANR<\/a> has selected the project BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) under the framework &#8220;appel \u00e0 projets g\u00e9n\u00e9rique 2020&#8221;.<\/p>\n<ul>\n<li><strong>DURATION<\/strong> : 48 months<\/li>\n<li><strong>PARTNERS<\/strong>: INRIA Nancy (leader), <span class=\"couleur_bleu\"><strong>CLEARSY<\/strong><\/span>, CRIL Lens, Universit\u00e9 de Li\u00e8ge<\/li>\n<\/ul>\n<ul><\/ul>\n<p>The BLaSST project targets bridging combinational and symbolic techniques in automatic theorem proving and validating the results for proof obligations generated from B models.<br \/>\nWork will be carried out on SAT-based encodings and optimized resolution techniques for proof, model generation, and lemma suggestion, as well as on encoding and reasoning techniques for expressive SMT-based formalisms.<br \/>\nCombining both lines of work, the expected scientific impact is an increase of the automation of solvers for expressive input languages by leveraging higher-order reasoning and enumerative instantiations for quantifiers over finite domains.<br \/>\nThe effectiveness of the techniques will be quantified by validation over industrial benchmarks that are known to be difficult for current reasoning engines. The industrial impact of BLaSST will be higher productivity of proof engineers. The benchmarks and improved solvers will be made openly available under permissive open-source licenses.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>ANR has selected the project BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) under the framework &#8220;appel \u00e0 projets g\u00e9n\u00e9rique 2020&#8221;.<\/p>\n","protected":false},"featured_media":17830,"template":"","class_list":["post-17829","recherche","type-recherche","status-publish","has-post-thumbnail","hentry"],"acf":[],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.1.1 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>BLASST - 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\/research-and-development\/blasst\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"BLASST - CLEARSY\" \/>\n<meta property=\"og:description\" content=\"ANR has selected the project BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) under the framework &quot;appel \u00e0 projets g\u00e9n\u00e9rique 2020&quot;.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/\" \/>\n<meta property=\"og:site_name\" content=\"CLEARSY\" \/>\n<meta property=\"article:modified_time\" content=\"2021-09-07T12:44:50+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg\" \/>\n\t<meta property=\"og:image:width\" content=\"1945\" \/>\n\t<meta property=\"og:image:height\" content=\"1046\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/jpeg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"1 minute\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/\",\"url\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/\",\"name\":\"BLASST - CLEARSY\",\"isPartOf\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage\"},\"image\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage\"},\"thumbnailUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg\",\"datePublished\":\"2021-09-07T12:41:37+00:00\",\"dateModified\":\"2021-09-07T12:44:50+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage\",\"url\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg\",\"contentUrl\":\"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg\",\"width\":1945,\"height\":1046},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\/\/www.clearsy.com\/en\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Research and development\",\"item\":\"https:\/\/www.clearsy.com\/en\/research-and-development\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"BLASST\"}]},{\"@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\/\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"BLASST - 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\/research-and-development\/blasst\/","og_locale":"en_US","og_type":"article","og_title":"BLASST - CLEARSY","og_description":"ANR has selected the project BLaSST (Enhancing B Language Reasoners with SAT and SMT Techniques) under the framework \"appel \u00e0 projets g\u00e9n\u00e9rique 2020\".","og_url":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/","og_site_name":"CLEARSY","article_modified_time":"2021-09-07T12:44:50+00:00","og_image":[{"width":1945,"height":1046,"url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg","type":"image\/jpeg"}],"twitter_card":"summary_large_image","twitter_misc":{"Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/","url":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/","name":"BLASST - CLEARSY","isPartOf":{"@id":"https:\/\/www.clearsy.com\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage"},"image":{"@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage"},"thumbnailUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg","datePublished":"2021-09-07T12:41:37+00:00","dateModified":"2021-09-07T12:44:50+00:00","breadcrumb":{"@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#primaryimage","url":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg","contentUrl":"https:\/\/www.clearsy.com\/wp-content\/uploads\/2021\/09\/logo-blasst-en.jpg","width":1945,"height":1046},{"@type":"BreadcrumbList","@id":"https:\/\/www.clearsy.com\/en\/research-and-development\/blasst\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.clearsy.com\/en\/"},{"@type":"ListItem","position":2,"name":"Research and development","item":"https:\/\/www.clearsy.com\/en\/research-and-development\/"},{"@type":"ListItem","position":3,"name":"BLASST"}]},{"@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\/"}}]}},"_links":{"self":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/recherche\/17829","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/recherche"}],"about":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/types\/recherche"}],"version-history":[{"count":2,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/recherche\/17829\/revisions"}],"predecessor-version":[{"id":17835,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/recherche\/17829\/revisions\/17835"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media\/17830"}],"wp:attachment":[{"href":"https:\/\/www.clearsy.com\/en\/wp-json\/wp\/v2\/media?parent=17829"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}