{"id":5503,"date":"2022-02-08T12:26:06","date_gmt":"2022-02-08T10:26:06","guid":{"rendered":"https:\/\/zen-cori.138-201-132-86.plesk.page\/?post_type=events&#038;p=5503"},"modified":"2022-07-25T11:54:41","modified_gmt":"2022-07-25T09:54:41","slug":"25th-mbmv-workshop","status":"publish","type":"events","link":"https:\/\/www.btc-embedded.com\/de\/events\/25th-mbmv-workshop\/","title":{"rendered":"25th MBMV Workshop"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-post\" data-elementor-id=\"5503\" class=\"elementor elementor-5503\" data-elementor-post-type=\"events\">\n\t\t\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-d26a8b4 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"d26a8b4\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-e230c73\" data-id=\"e230c73\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t<div class=\"elementor-element elementor-element-9c6de56 elementor-widget elementor-widget-text-editor\" data-id=\"9c6de56\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t<p><strong>Date: February 17th, 2022<\/strong><\/p><p><strong>Location: Online<\/strong><\/p><p>BTC Embedded Systems will join the 25th MBMV Workshop and give a talk about &#8222;Detection and Elimination of Constants to Strengthen k-Induction&#8220;<\/p><p>Please find more information about the event\u00a0<a href=\"https:\/\/www.vde.com\/de\/itg\/veranstaltungen\/veranstaltung?id=20735&amp;type=vde%7Cvdb\" target=\"_blank\" rel=\"noopener\">here<\/a>.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<section class=\"elementor-section elementor-inner-section elementor-element elementor-element-bad596c elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"bad596c\" data-element_type=\"section\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-default\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-inner-column elementor-element elementor-element-7efc0bb\" data-id=\"7efc0bb\" data-element_type=\"column\" data-settings=\"{&quot;background_background&quot;:&quot;classic&quot;}\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t<div class=\"elementor-element elementor-element-fd08004 elementor-widget elementor-widget-text-editor\" data-id=\"fd08004\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t<h3>&#8222;Detection and Elimination of Constants to Strengthen k-Induction&#8220;<\/h3><p>Presenter: Lukas Mentel<\/p><p><strong>Abstract:<\/strong><\/p><p>During the last years, software model checking has become a reliable technique for the verification of software that is used in safety-critical environments &#8212; e.g. to prove the absence of dead code.<br \/>One technique to perform such proofs is k-induction which considers in its induction step the property and transition relation but ignores the initial states. Therefore, k-induction is very sensitive regarding the encoding of variables which have a constant value &#8212; in particular if the encoding depends on the initial states. A recent bachelor thesis addresses this problem. In this paper, we present the main results, describe the integration into the commercial test and verification tool BTC EmbeddedPlatform and evaluate our implementation on a benchmark set with verification tasks originating from the automotive domain.<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>BTC Embedded Systems will join the 25th MBMV Workshop and give a talk about &#8222;Detection and Elimination of Constants to Strengthen k-Induction&#8220;<\/p>\n","protected":false},"featured_media":0,"template":"elementor_theme","event_type":[57,58],"class_list":["post-5503","events","type-events","status-publish","hentry","event_type-webinar","event_type-workshop"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/events\/5503","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/events"}],"about":[{"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/types\/events"}],"version-history":[{"count":0,"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/events\/5503\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/media?parent=5503"}],"wp:term":[{"taxonomy":"event_type","embeddable":true,"href":"https:\/\/www.btc-embedded.com\/de\/wp-json\/wp\/v2\/event_type?post=5503"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}