{"id":2090,"date":"2021-10-05T07:40:00","date_gmt":"2021-10-05T06:40:00","guid":{"rendered":"https:\/\/www.systerel.fr\/en\/?p=2090"},"modified":"2023-03-24T15:00:53","modified_gmt":"2023-03-24T14:00:53","slug":"hll-language-for-formal-verification-of-critical-software-or-systems","status":"publish","type":"post","link":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/","title":{"rendered":"HLL language for formal verification of critical software or systems"},"content":{"rendered":"\n

Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the next HLL Forum review in order to converge on the new definition of the language in collaboration with the other actors of the community.<\/strong><\/p>\n\n\n\n

These evolutions will facilitate modelling, improve the readability of models and allow users to build finer proof environments.<\/p>\n\n\n\n

Thanks to these evolutions, the HLL is enriched with the following functionalities:<\/p>\n\n\n\n

– syntax now allows the use of tuples in an assignment<\/p>\n\n\n\n

– functions become a generalization of arrays<\/p>\n\n\n\n

– a newSELECT quantifier allowing the user to query its model for the possible singleton defined by an expression<\/p>\n\n\n\n

– nil generalization for models correct definition<\/p>\n\n\n\n

– management of empty types<\/p>\n\n\n\n

– quantification on types<\/p>\n\n\n\n

– generalization of elementhood<\/p>\n\n\n\n

– quantification on composite types<\/p>\n\n\n\n

– POs can now be collections<\/p>\n\n\n\n

<\/p>\n\n\n\n

The document is available in preview here<\/a>, feel free to download it.<\/p>\n\n\n\n

<\/p>\n\n\n\n

<\/p>\n\n\n\nTo know more about the HLL language<\/a>\n\n\nOur formal verification offer Systerel Smart Solver around this language<\/a>\n\n\n\n

<\/p>\n\n\n\n

<\/p>\n","protected":false},"excerpt":{"rendered":"

Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the next HLL Forum review in order to converge on the new definition of the language in collaboration with the other actors of the community.<\/p>\n","protected":false},"author":19,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":true,"template":"","format":"standard","meta":{"footnotes":""},"categories":[14],"tags":[],"class_list":["post-2090","post","type-post","status-publish","format-standard","hentry","category-formal-methods"],"yoast_head":"\nHLL language for formal verification of critical software or systems<\/title>\n<meta name=\"description\" content=\"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3\" \/>\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\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/\" \/>\n<meta property=\"og:locale\" content=\"en_US\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"HLL language for formal verification of critical software or systems\" \/>\n<meta property=\"og:description\" content=\"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/\" \/>\n<meta property=\"og:site_name\" content=\"Systerel English\" \/>\n<meta property=\"article:published_time\" content=\"2021-10-05T06:40:00+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2023-03-24T14:00:53+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2021\/09\/590_393_HLL.png\" \/>\n\t<meta property=\"og:image:width\" content=\"590\" \/>\n\t<meta property=\"og:image:height\" content=\"393\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/png\" \/>\n<meta name=\"author\" content=\"coralie\" \/>\n<meta name=\"twitter:label1\" content=\"Written by\" \/>\n\t<meta name=\"twitter:data1\" content=\"coralie\" \/>\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.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/\"},\"author\":{\"name\":\"coralie\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\"},\"headline\":\"HLL language for formal verification of critical software or systems\",\"datePublished\":\"2021-10-05T06:40:00+00:00\",\"dateModified\":\"2023-03-24T14:00:53+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/\"},\"wordCount\":204,\"articleSection\":[\"Formal Methods\"],\"inLanguage\":\"en-US\"},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/\",\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/\",\"name\":\"HLL language for formal verification of critical software or systems\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#website\"},\"datePublished\":\"2021-10-05T06:40:00+00:00\",\"dateModified\":\"2023-03-24T14:00:53+00:00\",\"author\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\"},\"description\":\"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/#breadcrumb\"},\"inLanguage\":\"en-US\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/hll-language-for-formal-verification-of-critical-software-or-systems\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"HLL language for formal verification of critical software or systems\"}]},{\"@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\"},{\"@type\":\"Person\",\"@id\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/#\\\/schema\\\/person\\\/8bfeb6ce2fe1bd6d0344938e6e5786db\",\"name\":\"coralie\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"en-US\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g\",\"caption\":\"coralie\"},\"url\":\"https:\\\/\\\/www.systerel.fr\\\/en\\\/news\\\/author\\\/coralie\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"HLL language for formal verification of critical software or systems","description":"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3","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\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/","og_locale":"en_US","og_type":"article","og_title":"HLL language for formal verification of critical software or systems","og_description":"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3","og_url":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/","og_site_name":"Systerel English","article_published_time":"2021-10-05T06:40:00+00:00","article_modified_time":"2023-03-24T14:00:53+00:00","og_image":[{"width":590,"height":393,"url":"https:\/\/www.systerel.fr\/en\/wp-content\/uploads\/sites\/3\/2021\/09\/590_393_HLL.png","type":"image\/png"}],"author":"coralie","twitter_misc":{"Written by":"coralie","Est. reading time":"1 minute"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/#article","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/"},"author":{"name":"coralie","@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db"},"headline":"HLL language for formal verification of critical software or systems","datePublished":"2021-10-05T06:40:00+00:00","dateModified":"2023-03-24T14:00:53+00:00","mainEntityOfPage":{"@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/"},"wordCount":204,"articleSection":["Formal Methods"],"inLanguage":"en-US"},{"@type":"WebPage","@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/","url":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/","name":"HLL language for formal verification of critical software or systems","isPartOf":{"@id":"https:\/\/www.systerel.fr\/en\/#website"},"datePublished":"2021-10-05T06:40:00+00:00","dateModified":"2023-03-24T14:00:53+00:00","author":{"@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db"},"description":"Systerel publishes a new version of the HLL specification document (HLL LFD) and submits it to the HLL Forum for review in order to formally converge on the new language definition in collaboration with the other actors of the community.Document available here => lien page To know more about the HLL language => lien page HLL site SysterelTo know more about our formal verification offer Systerel Smart Solver around this language => lien page S3","breadcrumb":{"@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/#breadcrumb"},"inLanguage":"en-US","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.systerel.fr\/en\/news\/hll-language-for-formal-verification-of-critical-software-or-systems\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/www.systerel.fr\/en\/"},{"@type":"ListItem","position":2,"name":"HLL language for formal verification of critical software or systems"}]},{"@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"},{"@type":"Person","@id":"https:\/\/www.systerel.fr\/en\/#\/schema\/person\/8bfeb6ce2fe1bd6d0344938e6e5786db","name":"coralie","image":{"@type":"ImageObject","inLanguage":"en-US","@id":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/b4786b8196c518e7fe48f6c85b4c2a879c52aeb92e2614e404638a55e9b1840d?s=96&d=mm&r=g","caption":"coralie"},"url":"https:\/\/www.systerel.fr\/en\/news\/author\/coralie\/"}]}},"_links":{"self":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/2090","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/users\/19"}],"replies":[{"embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/comments?post=2090"}],"version-history":[{"count":6,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/2090\/revisions"}],"predecessor-version":[{"id":2154,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/posts\/2090\/revisions\/2154"}],"wp:attachment":[{"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/media?parent=2090"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/categories?post=2090"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.systerel.fr\/en\/wp-json\/wp\/v2\/tags?post=2090"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}