{"id":722,"date":"2014-10-08T14:07:49","date_gmt":"2014-10-08T13:07:49","guid":{"rendered":"http:\/\/www.systerel.fr\/en\/?page_id=722"},"modified":"2026-02-02T11:42:29","modified_gmt":"2026-02-02T10:42:29","slug":"systerel-smart-solver","status":"publish","type":"page","link":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/","title":{"rendered":"Systerel Smart Solver"},"content":{"rendered":"<div class=\"wp-block-image\">\n<figure class=\"aligncenter is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"512\" src=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def-1024x512.png\" alt=\"S3 boxes def\" class=\"wp-image-720\" style=\"width:600px\" srcset=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def-1024x512.png 1024w, https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def-300x150.png 300w, https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def.png 1200w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n<\/div>\n\n\n<p><\/p>\n\n\n\n<h2 class=\"wp-block-heading\"><span style=\"color: #004187;\">Static analysis and formal proof of systems and software<\/span><\/h2>\n\n\n\n<p>Systerel offers a range of industrially proven solutions using Model Checking based technologies for the static analysis and formal proof of systems and software.<br>Systerel Smart Solver (S3), a SAT based analysis tool is central to these solutions.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">A wide range of services<\/h2>\n\n\n\n<p>In conjunction with specialized translators and specific tools, S3 is able to offer a variety of services:<\/p>\n\n\n<section class=\"block  blanc avec-onglet\"><\/p>\n<ul>\n<li>Static code analysis<\/li>\n<li>Proof of safety properties &#8211; certification<\/li>\n<li>Proof of user properties with counter examples analysis tools<\/li>\n<li>Automatic test case generation (functional or structural)<\/li>\n<\/ul>\n<p><\/section>\n\n\n\n<h2 class=\"wp-block-heading\">Synopsis<\/h2>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"aligncenter\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"472\" src=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3_generique_site_en-1024x472.png\" alt=\"S3_generique_site_en\" class=\"wp-image-881\" srcset=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3_generique_site_en-1024x472.png 1024w, https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3_generique_site_en-300x138.png 300w, https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3_generique_site_en.png 1780w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n<\/div>\n\n\n<p><\/p>\n\n\n<section class=\"block  &#8221;blanc\"><\/p>\n<ol>\n<li>Specification of the analysis goal: safety properties, test objectives, optimization criteria,&#8230;<\/li>\n<li>Formalization in HLL (High Level Language) by an application field modeler<\/li>\n<li>Automatic translation of the system \u00a0into an HLL model using a specialized translator (C, Ada, SCADE,\u2026)<\/li>\n<li>Analysis of the system and creation of the results (proofs, counter-examples, scenarios, tests,\u2026)<\/li>\n<\/ol>\n<p><\/section>\n\n\n\n<h2 class=\"wp-block-heading\">Benefits<\/h2>\n\n\n<section class=\"block  blanc avec-onglet\"><\/p>\n<ul>\n<li>Automated analyses and proofs<\/li>\n<li>Analysis completeness<\/li>\n<li>Exact modeling (no abstractions)<\/li>\n<li>Compliant with certification processes<\/li>\n<li>Dedicated team of specialists of the technology and tools<\/li>\n<\/ul>\n<p><\/section>\n\n\n\n<h2 class=\"wp-block-heading\">Functionalities<\/h2>\n\n\n<section class=\"block  blanc avec-onglet\"><\/p>\n<ul>\n<li>Static code analysis: absence of unspecified behaviors (OOB, UMR, OVF, DIV0), absence of unreachable and dead code<\/li>\n<li>Proof of user-defined properties<\/li>\n<li>Counter-examples analysis of falsified properties<\/li>\n<li>Automatic test case generation (functional or structural)<\/li>\n<li>Equivalence proof between specification and code, or between diversified codes<\/li>\n<\/ul>\n<p>Languages: C (C99 with some restrictions), Ada (subset), SCADE (v5,v6)<\/p>\n<p><\/section>\n\n\n\n<h2 class=\"wp-block-heading\">Certifiable Systerel Smart Solver (cS3) <figure><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-878 size-medium\" src=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/logo_certifiable-smart-solver-300x80.png\" alt=\"logo_certifiable-smart-solver\" width=\"300\" height=\"80\" srcset=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/logo_certifiable-smart-solver-300x80.png 300w, https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/logo_certifiable-smart-solver-1024x273.png 1024w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/figure><\/h2>\n\n\n<section class=\"block  blanc avec-onglet\"><\/p>\n<ul>\n<li>Certifiable analyses of the conformity of a system with a set of properties (safety, specification\u2026)<\/li>\n<li>According to the EN 50128:2011 norm, tool class T2 for SIL-4 systems<\/li>\n<li>\n<div id=\"tts_button\"><span id=\"result_box\" class=\"\" lang=\"fr\"><span class=\"hps\">Based on diversification, sequential equivalence checking and a posteriori proofs verification<\/span><\/span><\/div>\n<\/li>\n<\/ul>\n<p><\/section>\n\n\n\n<h2 class=\"wp-block-heading\">Industrial applications<\/h2>\n\n\n\n<p>Safety verification for a wide range of systems, including:<\/p>\n\n\n<section class=\"block  blanc avec-onglet\"><\/p>\n<ul>\n<li>Railway Interlocking systems (relay-based and computerized)<\/li>\n<li>CBTC (Communication-Based Train Control System)<\/li>\n<li>ERTMS (European Railway Traffic Management System)<\/li>\n<li>Avionic air flow regulation systems<\/li>\n<\/ul>\n<p><\/section>\n\n\n\n<p><strong>Systerel Smart Solver is a powerful proof solution. It increases confidence in the security level of a system while considerably reducing the time and cost of validation.<\/strong><\/p>\n\n\n\n<p>Various measurements carried out on industrial-scale projects show significant performance gains in the validation of safety properties: validation activities that previously took several months to complete are now done in a matter of hours.<\/p>\n\n\n\n<p>The application of Systerel Smart Solver on an industrial scale by major rail industry players (Hitachi, Alstom, RATP, SNCF, etc.), and the demonstration, in representative cases, of its ability to address the vast majority of interlocking systems currently deployed by SNCF for example, confirm the maturity of the implementation of formal verification for the development and deployment of operational interlocking systems.<\/p>\n\n\n\n<p>For academic experimentations or prototyping needs, Systerel gives access to licences of the Systerel Smart Solver. Systerel provided such licences to the French national aerospace research center (<a href=\"https:\/\/www.onera.fr\/\" target=\"_blank\" rel=\"noopener noreferrer\">ONERA<\/a>).<\/p>\n\n\n<a class=\"btn from-shortcode \" href=\"mailto:contact@systerel.fr\">Contact us<\/a>\n","protected":false},"excerpt":{"rendered":"<p>Formal verification of systems and software developed  in SCADE, C, Ada<\/p>\n","protected":false},"author":4,"featured_media":0,"parent":1119,"menu_order":5,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-722","page","type-page","status-publish","hentry"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v27.5 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Systerel Smart Solver - Systerel English<\/title>\n<meta name=\"description\" content=\"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.\" \/>\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.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Systerel Smart Solver - Systerel English\" \/>\n<meta property=\"og:description\" content=\"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/\" \/>\n<meta property=\"og:site_name\" content=\"Systerel English\" \/>\n<meta property=\"article:modified_time\" content=\"2026-02-02T10:42:29+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def.png\" \/>\n\t<meta property=\"og:image:width\" content=\"1200\" \/>\n\t<meta property=\"og:image:height\" content=\"600\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/png\" \/>\n<meta name=\"twitter:label1\" content=\"Est. reading time\" \/>\n\t<meta name=\"twitter:data1\" content=\"3 minutes\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/\",\"name\":\"Systerel Smart Solver - Systerel English\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2014\\\/10\\\/S3-boxes-def-1024x512.png\",\"datePublished\":\"2014-10-08T13:07:49+00:00\",\"dateModified\":\"2026-02-02T10:42:29+00:00\",\"description\":\"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/#primaryimage\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2014\\\/10\\\/S3-boxes-def.png\",\"contentUrl\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/wp-content\\\/uploads\\\/sites\\\/3\\\/2014\\\/10\\\/S3-boxes-def.png\",\"width\":1200,\"height\":600,\"caption\":\"Systerel Smart Solver for C, for Ada, for SCADE\"},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/systerel-smart-solver\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Innovation\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Products\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/innovation\\\/products\\\/\"},{\"@type\":\"ListItem\",\"position\":4,\"name\":\"Systerel Smart Solver\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\",\"name\":\"Systerel English\",\"description\":\"Safe real-time solutions\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"en-US\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Systerel Smart Solver - Systerel English","description":"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.","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.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/","og_locale":"en_US","og_type":"article","og_title":"Systerel Smart Solver - Systerel English","og_description":"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.","og_url":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/","og_site_name":"Systerel English","article_modified_time":"2026-02-02T10:42:29+00:00","og_image":[{"width":1200,"height":600,"url":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def.png","type":"image\/png"}],"twitter_misc":{"Est. reading time":"3 minutes"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/","url":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/","name":"Systerel Smart Solver - Systerel English","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/#website"},"primaryImageOfPage":{"@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/#primaryimage"},"image":{"@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/#primaryimage"},"thumbnailUrl":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def-1024x512.png","datePublished":"2014-10-08T13:07:49+00:00","dateModified":"2026-02-02T10:42:29+00:00","description":"Systerel Smart Solver provides formal proof for systems and software and automated test case generation using Model Checking and HLL language.","breadcrumb":{"@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/"]}]},{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/#primaryimage","url":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def.png","contentUrl":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2014\/10\/S3-boxes-def.png","width":1200,"height":600,"caption":"Systerel Smart Solver for C, for Ada, for SCADE"},{"@type":"BreadcrumbList","@id":"https:\/\/www.systerel.fr\/en\/innovation\/products\/systerel-smart-solver\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.systerel.fr\/en\/"},{"@type":"ListItem","position":2,"name":"Innovation","item":"https:\/\/www.systerel.fr\/en\/innovation\/"},{"@type":"ListItem","position":3,"name":"Products","item":"https:\/\/www.systerel.fr\/en\/innovation\/products\/"},{"@type":"ListItem","position":4,"name":"Systerel Smart Solver"}]},{"@type":"WebSite","@id":"https:\/\/www.systerel.fr\/en\/#website","url":"https:\/\/www.systerel.fr\/en\/","name":"Systerel English","description":"Safe real-time solutions","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.systerel.fr\/en\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"en-US"}]}},"_links":{"self":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/722","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/comments?post=722"}],"version-history":[{"count":22,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/722\/revisions"}],"predecessor-version":[{"id":3815,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/722\/revisions\/3815"}],"up":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/pages\/1119"}],"wp:attachment":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media?parent=722"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}