{"id":303,"date":"2018-02-28T19:17:30","date_gmt":"2018-02-28T19:17:30","guid":{"rendered":"https:\/\/from2021.cs.unibuc.ro\/?page_id=303"},"modified":"2021-11-26T15:39:38","modified_gmt":"2021-11-26T15:39:38","slug":"1-page","status":"publish","type":"page","link":"https:\/\/from2021.cs.unibuc.ro\/","title":{"rendered":"One Page Website"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"303\" class=\"elementor elementor-303\" data-elementor-settings=\"[]\">\n\t\t\t\t\t\t\t<div class=\"elementor-section-wrap\">\n\t\t\t\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-be4df7a elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"be4df7a\" 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-31d76ac\" data-id=\"31d76ac\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-da78b07 elementor-widget elementor-widget-heading\" data-id=\"da78b07\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">WORKING FORMAL METHODS SYMPOSIUM<br>December 8-9, 2021, Timi\u0219oara, Romania<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-bd27184 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"bd27184\" 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-c8f113f\" data-id=\"c8f113f\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-2d00790 elementor-widget elementor-widget-heading\" data-id=\"2d00790\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h4 class=\"elementor-heading-title elementor-size-default\">In conjunction with SYNASC 2021<\/h4>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-e5c8160 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"e5c8160\" 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-de3d76d\" data-id=\"de3d76d\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-fb08938 elementor-widget elementor-widget-text-editor\" data-id=\"fb08938\" 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<p>Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and\/or make the formal methods to work by creating or using software tools that apply theoretical contributions. Formal methods emphasize the use of mathematical techniques and rigor for developing software and hardware. They can be used to specify, verify, and analyse systems at any stage in their life cycle: requirements engineering, modeling, design, architecture, implementation, testing, maintenance and evolution. This assumes on one hand the development of adequate mathematical methods and frameworks and on the other hand the development of tools that help the user effectively apply these methods\/frameworks.<\/p>\n<p>FROM symposiums are&nbsp; organized by the <a href=\"https:\/\/fmi.unibuc.ro\/en\/\">Faculty of Mathematics and Computer Science of the University of Bucharest<\/a>, the&nbsp;<a href=\"http:\/\/www.cs.ubbcluj.ro\/\" target=\"_blank\" rel=\"noopener\">Faculty of Mathematics and Computer Science of the Babes-Bolyai University of Cluj-Napoca<\/a>, the <a href=\"https:\/\/www.info.uaic.ro\/en\/home-page-2\/\">Faculty of Computer Science of the Alexandru Ioan Cuza University of Iasi<\/a>, and the&nbsp; <a href=\"https:\/\/www.info.uvt.ro\/en\/\">Faculty of Mathematics and Computer Science of the West University of Timi\u0219oara<\/a>.<\/p>\n<p>FROM 2021 is the fifth event in a yearly workshop series. <a href=\"http:\/\/unibuc.ro\/~conference\/from2017\" target=\"_blank\" rel=\"noopener\">The first edition<\/a> was held in 2017 in Bucharest,&nbsp;<a href=\"http:\/\/fmse.info.uaic.ro\/event\/from-2018\" target=\"_blank\" rel=\"noopener\">the second edition<\/a> was held in 2018 in Ia\u015fi, <a href=\"http:\/\/from2019.projects.uvt.ro\" target=\"_blank\" rel=\"noopener\">the third edition<\/a> was held in 2019 in Timi\u015foara, while <a href=\"http:\/\/www.cs.ubbcluj.ro\/from2020\/\" target=\"_blank\" rel=\"noopener\">the fourth edition <\/a>was organized in Cluj-Napoca as a virtual event due to the COVID-19 pandemic.<\/p>\n<p>FROM 2021 is an associated workshop of&nbsp; <a href=\"https:\/\/synasc.ro\/2021\/\" target=\"_blank\" rel=\"noopener\">SYNASC 2021<\/a>.<\/p>\n<p>The program of the symposium includes invited lectures and regular contributions. Submissions on the general topics of formal methods, theoretical computer science, logic and applications are welcome.<\/p>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-82e8673 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"82e8673\" 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-c688aae\" data-id=\"c688aae\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-e273ffc elementor-widget elementor-widget-heading\" data-id=\"e273ffc\" data-element_type=\"widget\" id=\"dates\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Important Dates<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-8dca514 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"8dca514\" 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-85d703a\" data-id=\"85d703a\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-3c4ab2a elementor-widget elementor-widget-text-editor\" data-id=\"3c4ab2a\" 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<ul><li><b>September 29, 2021<\/b>: Deadline for full paper submission.<\/li><li><b>October 7, 2021<\/b>: Notification of acceptance.<\/li><li><b>October 15 2021<\/b>: Submission of revised papers.<\/li><li><b>October 15, 2021<\/b>: Registration.<\/li><li><b>December 8-9 2021<\/b>: Symposium days.<\/li><\/ul>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-6a2b220 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"6a2b220\" 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-3d093ec\" data-id=\"3d093ec\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-69ee904 elementor-widget elementor-widget-menu-anchor\" data-id=\"69ee904\" data-element_type=\"widget\" data-widget_type=\"menu-anchor.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div id=\"cfp\" class=\"elementor-menu-anchor\"><\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-99ccb59 elementor-widget elementor-widget-heading\" data-id=\"99ccb59\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Call for papers<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-fb4d87e elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"fb4d87e\" 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-4c98418\" data-id=\"4c98418\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-772ea89 elementor-widget elementor-widget-text-editor\" data-id=\"772ea89\" 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<p><a href=\"https:\/\/drive.google.com\/file\/d\/175C1MzFwWHOVcrzpGj7d_EVuzuP04S5O\/view?usp=sharing\" target=\"_blank\" rel=\"noopener\"><b>CFP &#8211; September 20, 2021<\/b><\/a><\/p>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-e1c9935 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"e1c9935\" 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-072551e\" data-id=\"072551e\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-793cadc elementor-widget elementor-widget-heading\" data-id=\"793cadc\" data-element_type=\"widget\" id=\"invited\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Invited Speakers<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-74ef898 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"74ef898\" 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-a256eb9\" data-id=\"a256eb9\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap\">\n\t\t\t\t\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-5acfe804 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"5acfe804\" 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-335a32a5\" data-id=\"335a32a5\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-36508a5 elementor-position-left elementor-vertical-align-top elementor-widget elementor-widget-image-box\" data-id=\"36508a5\" data-element_type=\"widget\" data-widget_type=\"image-box.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<div class=\"elementor-image-box-wrapper\"><figure class=\"elementor-image-box-img\"><a href=\"https:\/\/fmi.uni-stuttgart.de\/ti\/team\/diekert\/\" target=\"_blank\"><img loading=\"lazy\" decoding=\"async\" width=\"204\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Diekert-204x300.jpg\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Diekert-204x300.jpg 204w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Diekert.jpg 272w\" sizes=\"auto, (max-width: 204px) 100vw, 204px\" \/><\/a><\/figure><div class=\"elementor-image-box-content\"><h4 class=\"elementor-image-box-title\"><a href=\"https:\/\/fmi.uni-stuttgart.de\/ti\/team\/diekert\/\" target=\"_blank\">VOLKER DIEKERT<br>University of Stuttgart<\/a><\/h4><p class=\"elementor-image-box-description\"><i>Decidability of membership problems in 2 \u00d7 2 matrices over rational numbers\n<\/i><br> <br><div style= \"text-align: justify\">The talk is based on a joint work with Igor Potapov and Pavel Semukhin (Liverpool, UK).\nIt appeared as a conference abstract at ISSAC 2020. Our results relate numerical problems\non matrices over the rationals to symbolic algorithms on words and finite automata. <br>Using\nexact algebraic algorithms and symbolic computation, we prove new decidability results for\n2 \u00d7 2 matrices over \u211a. Namely, we introduce a notion of <I>flat rational sets<\/i>: if M is a monoid\nand N \u2264 M is its submonoid, then flat rational sets of M relative to N are finite unions of\nthe form L<sub>0<\/sub>g<sub>1<\/sub>L<sub>1<\/sub>\u2026g<sub>t<\/sub>L<sub>t<\/sub> where all L<sub>i<\/sub>s are rational subsets of N and g<sub>i <\/sub>\u2208 M. We give quite\ngeneral sufficient conditions under which \nflat rational sets form an effective relative Boolean algebra. <br> As a corollary, we obtain that the emptiness problem for Boolean combinations of flat rational subsets of GL(2;\u211a) over GL(2;\u2124) is decidable. On the other hand, there is\nsome evidence supporting our conjecture that the membership problem for rational subsets\nof GL(2;\u211a) is undecidable.<\/div><\/p><\/div><\/div>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-67363dd elementor-position-left elementor-vertical-align-top elementor-widget elementor-widget-image-box\" data-id=\"67363dd\" data-element_type=\"widget\" data-widget_type=\"image-box.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<div class=\"elementor-image-box-wrapper\"><figure class=\"elementor-image-box-img\"><a href=\"https:\/\/www.linkedin.com\/in\/gavrilutdragos\" target=\"_blank\"><img loading=\"lazy\" decoding=\"async\" width=\"204\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/dragosgavrilut260-400jpg-204x300.jpg\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/dragosgavrilut260-400jpg-204x300.jpg 204w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/dragosgavrilut260-400jpg.jpg 272w\" sizes=\"auto, (max-width: 204px) 100vw, 204px\" \/><\/a><\/figure><div class=\"elementor-image-box-content\"><h4 class=\"elementor-image-box-title\"><a href=\"https:\/\/www.linkedin.com\/in\/gavrilutdragos\" target=\"_blank\">DRAGO\u0218 GAVRILU\u021a<br>Bitdefender and \"Alexandru Ioan Cuza\" University of Ia\u0219i<br><\/a><\/h4><p class=\"elementor-image-box-description\"><i>IoT security: The good the bad and the ugly\n<\/i><br>\n<br><div style= \"text-align: justify\">IoT industry have grown in the last couple of years to the point where many people are now using one or two IoT devices. Analysts like Gartner and Forrester predicted this growth and raised several security concerns (most of them being related to privacy and access to personal data). In particular for consumer users, this may also represent other security ricks such as data exfiltration. This presentation focuses on presenting the risks that come with IoT devices (in terms of privacy and access). As a practical aspect, some newly discovered IoT vulnerabilities ( in IoT devices like web-cameras or baby-monitors) with details on how these vulnerabilities were discovered and how they work will be presented.\n<\/div><\/p><\/div><\/div>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-8700fdb elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"8700fdb\" 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-b6edfc7\" data-id=\"b6edfc7\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-c016193 elementor-position-left elementor-vertical-align-top elementor-widget elementor-widget-image-box\" data-id=\"c016193\" data-element_type=\"widget\" data-widget_type=\"image-box.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<div class=\"elementor-image-box-wrapper\"><figure class=\"elementor-image-box-img\"><a href=\"http:\/\/nts.imag.fr\/index.php\/Radu_Iosif\" target=\"_blank\"><img loading=\"lazy\" decoding=\"async\" width=\"204\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/RaduIosif272-400-204x300.png\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/RaduIosif272-400-204x300.png 204w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/RaduIosif272-400.png 272w\" sizes=\"auto, (max-width: 204px) 100vw, 204px\" \/><\/a><\/figure><div class=\"elementor-image-box-content\"><h4 class=\"elementor-image-box-title\"><a href=\"http:\/\/nts.imag.fr\/index.php\/Radu_Iosif\" target=\"_blank\">RADU IOSIF<br>VERIMAG - CNRS - University of Grenoble Alpes<\/a><\/h4><p class=\"elementor-image-box-description\"><i>Local Reasoning about Parameterized Reconfigurable Distributed Systems\n<\/i><br> <br><div style= \"text-align: justify\">This paper presents a Hoare-style calculus for formal reasoning about reconfiguration programs of distributed systems. Such programs delete or create interactions or components while the system components change state according to their local behaviour. Our proof calculus uses a configuration logic that supports local reasoning and that relies on inductive predicates to describe distributed systems with an unbounded number of components. The validity of reconfiguration programs relies on havoc invariants, assertions about the ongoing interactions in the system. We present a proof system for such invariants in an assume\/rely-guarantee style. We illustrate the feasibility of our approach by proving the correctness of self-adjustable tree architectures and provide tight complexity bounds for entailment checking in the configuration logic.<br>Joint work with Emma Ahrens and Joost-Pieter Katoen (RWTH Aachen) and Marius Bozga (VERIMAG).<\/div><\/p><\/div><\/div>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-6af9af4 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"6af9af4\" 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-12413d2\" data-id=\"12413d2\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-1caf8c6 elementor-position-left elementor-vertical-align-top elementor-widget elementor-widget-image-box\" data-id=\"1caf8c6\" data-element_type=\"widget\" data-widget_type=\"image-box.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<div class=\"elementor-image-box-wrapper\"><figure class=\"elementor-image-box-img\"><a href=\"https:\/\/www.andreipopescu.uk\" target=\"_blank\"><img loading=\"lazy\" decoding=\"async\" width=\"204\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Andrei_Popescu_2020_272x400-204x300.jpg\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Andrei_Popescu_2020_272x400-204x300.jpg 204w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/Andrei_Popescu_2020_272x400.jpg 272w\" sizes=\"auto, (max-width: 204px) 100vw, 204px\" \/><\/a><\/figure><div class=\"elementor-image-box-content\"><h4 class=\"elementor-image-box-title\"><a href=\"https:\/\/www.andreipopescu.uk\" target=\"_blank\">ANDREI POPESCU<br>University of Sheffield<\/a><\/h4><p class=\"elementor-image-box-description\"><i>Types-to-Sets for Theorem Proving in Higher-Order Logic <\/i> <br> <br><div style= \"text-align: justify\"> Users of interactive theorem provers based on Higher-Order Logic (such as HOL4 and Isabelle\/HOL) find it very convenient to \"ride\" the HOL type system when defining concepts and reasoning about them -- within a paradigm that can be called *type-based reasoning*. However, to achieve higher flexibility, users often need to resort to *set-based reasoning*, which is more bureaucratic and less supported by automation. In previous work with Ondrej Kuncar, I developed a mechanism called Types-to-Sets that allows one to make the best of both worlds by offering a bridge between the simpler type-based theorems and the heavier set-based ones. In recent work jointly with Dmitriy Traytel I show that, contrary to the previous belief, the rules for moving from types to sets are admissible in the standard Higher-Order Logic used in theorem provers, so no extension of the axiomatization base is required. In this talk, I will motivate and introduce the Types-to-Sets framework, and will present the recent admissibility result and its connection to other concepts such as Reynolds-style parametricity and compositional (co)datatypes.<\/div><\/p><\/div><\/div>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-7969fe6 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7969fe6\" 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-55d3b02\" data-id=\"55d3b02\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-c01ab4d elementor-position-left elementor-vertical-align-top elementor-widget elementor-widget-image-box\" data-id=\"c01ab4d\" data-element_type=\"widget\" data-widget_type=\"image-box.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<div class=\"elementor-image-box-wrapper\"><figure class=\"elementor-image-box-img\"><a href=\"http:\/\/florinstoican.com\/os\/academic\" target=\"_blank\"><img loading=\"lazy\" decoding=\"async\" width=\"204\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/FlorinStoican272-400-204x300.jpg\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/FlorinStoican272-400-204x300.jpg 204w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/FlorinStoican272-400.jpg 272w\" sizes=\"auto, (max-width: 204px) 100vw, 204px\" \/><\/a><\/figure><div class=\"elementor-image-box-content\"><h4 class=\"elementor-image-box-title\"><a href=\"http:\/\/florinstoican.com\/os\/academic\" target=\"_blank\">FLORIN STOICAN<br>Polytechnic University of Bucharest <\/a><\/h4><p class=\"elementor-image-box-description\"><i>On the use of spline functions in motion planning<\/i><br> <br><div style= \"text-align: justify\">B-spline and NURBS functions are popular choices for describing trajectories associated with nonlinear dynamics and for imposing continuous-time constraint validation. Exploiting their properties (local support, convexity and positivity) usually leads to sufficient conditions which are conservative and difficult to handle as part of an optimization problem.<br>In this talk I will present several methods which reduce the conservatism and complexity of the approach. First, I will make use of knot refinement strategies to improve arbitrarily-well on the sufficient conditions. Second, I will provide approximate solutions which reduce significantly the computational effort at the price of a moderate loss in performance. The approaches are validated for a motion planning problem where off-line trajectories with obstacle(s) avoidance guarantees are generated.<\/div><\/p><\/div><\/div>\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-ece0ff5 elementor-widget elementor-widget-heading\" data-id=\"ece0ff5\" data-element_type=\"widget\" id=\"commitees\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Commitees<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-3d10b0f elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"3d10b0f\" 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-b6e1816\" data-id=\"b6e1816\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-fc013e2 elementor-widget elementor-widget-text-editor\" data-id=\"fc013e2\" 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<h4>Program Commitee<\/h4>\n<table dir=\"ltr\" border=\"1\" cellspacing=\"0\" cellpadding=\"0\">\n<colgroup>\n<col width=\"470\"><\/colgroup>\n<tbody>\n<tr>\n<td data-sheets-value=\"{\">Andrei Arusoaie,  Alexandru Ioan Cuza University of Ia\u0219i<\/td>\n<\/tr>\n<tr>\n<\/tr><tr>\n<td data-sheets-value=\"{\">Adrian Cr\u0103ciun, West University of Timi\u0219oara<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Florin Cr\u0103ciun, Babe\u0219-Bolyai University of Cluj-Napoca<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">C\u0103t\u0103lin Dima, Universit\u00e9 Paris-Est Cr\u00e9teil<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Ioana Leu\u015ftean, University of Bucharest<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Lauren\u021biu Leu\u015ftean, University of Bucharest (Co-chair)<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Dorel Lucanu, Alexandru Ioan Cuza University of Ia\u0219i<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Mircea Marin, West University of Timi\u0219oara (Co-chair)<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Simona Motogna,  Babe\u0219-Bolyai University of Cluj-Napoca<\/td>\n<\/tr>\n<tr>\n<\/tr><tr>\n<td data-sheets-value=\"{\">David Nowak, CNRS &amp; University of Lille <\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Grigore Ro\u015fu, University of Illinois at Urbana-Champaign<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Vlad Rusu, INRIA Lille Nord Europe<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Viorica Sofronie-Stokkermans, University Koblenz-Landau<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<h4>Organising Commitee<\/h4>\n<table dir=\"ltr\" border=\"1\" cellspacing=\"0\" cellpadding=\"0\">\n<colgroup>\n<col width=\"378\"><\/colgroup>\n<tbody>\n<tr>\n<td data-sheets-value=\"{\">Isabela Dr\u0103mnesc, West University of Timi\u0219oara<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Mircea Marin, West University of Timi\u0219oara (Chair)<\/td>\n<\/tr>\n<tr>\n<td data-sheets-value=\"{\">Natalia Ozunu (Moang\u0103), University of Bucharest<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-f7db772 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"f7db772\" 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-dc02082\" data-id=\"dc02082\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-7627fd0 elementor-widget elementor-widget-heading\" data-id=\"7627fd0\" data-element_type=\"widget\" id=\"registration\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Registration<\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-df71d0b elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"df71d0b\" 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-74d1e8b\" data-id=\"74d1e8b\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-3c23221 elementor-widget elementor-widget-text-editor\" data-id=\"3c23221\" 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<p>The registration fee is 100 Euro.<br \/>It covers the symposium kit, refreshments during breaks, lunches, symposium dinner, publication.<br \/>The registration is open until November 1, 2021. The registration form is available <a href=\"https:\/\/indico.ieat.ro\/event\/3\/registrations\/2\/\" target=\"_blank\" rel=\"noopener\">here<\/a>.<\/p>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-b9589e7 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"b9589e7\" 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-56a4708\" data-id=\"56a4708\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-b2be8bb elementor-widget elementor-widget-heading\" data-id=\"b2be8bb\" data-element_type=\"widget\" id=\"program\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Program <\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-7a94899 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7a94899\" 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-81381e2\" data-id=\"81381e2\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-3e7239b elementor-widget elementor-widget-text-editor\" data-id=\"3e7239b\" 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<div class=\"date\" style=\"text-align: center; padding: 5pt 0pt; font-size: 16px; margin: 4pt 0pt; background-color: #7a8687; color: #000000; font-family: Arial, Helvetica, sans-serif; font-style: normal; font-weight: 400;\">Wednesday, December 8th<\/div>\n<div style=\"font-size: 12pt; background-color:#31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"font-size: 12pt; color: #666666; font-weight: bold;\">11:00-11:50<\/span><span style=\"font-size: 12pt;\">\u00a0<\/span><span style=\"font-size: 12pt; margin-left: 16pt;\">Session 9: FROM Invited Talk (1)<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person73.html\">Mircea Marin<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">11:00<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person284.html\">Volker Diekert<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Decidability of membership problems in 2 \u00d7 2 matrices over rational numbers\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:186050\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">12:10-12:50<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 11: FROM Workshop (1)<\/span><\/div>\n<div style=\"border-left: 1px solid #cccccc; border-right: 1px solid #cccccc; border-bottom: 1px solid #cccccc; margin: 0pt 0pt 3pt; padding: 3pt 3pt 3pt 5pt; background: #add8db; border-radius: 0px 0px 6px 6px; color: #666666; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<p style=\"margin-top: 0pt; margin-bottom: 0pt;\">Working Formal Methods Symposium<\/p>\n\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person41.html\">Adrian Craciun<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">12:10<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person271.html\">Horatiu Cheval<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Applications of the Lean theorem prover to proof mining\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:185967\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">12:30<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person92.html\">Mihai Prunescu<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Secure Multiparty Computation in arbitrary rings\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:186001\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">14:00-14:50<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 12: SYNASC and FROM Invited Talk (5)<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person93.html\">Ciprian Pungila<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room276.html\">Room SYNASC &#8211; main<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">14:00<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person286.html\">Dragos-Teodor Gavrilut<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">IoT security: The good the bad and the ugly\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:186042\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">15:10-16:00<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 13B: FROM Invited Talk (3)<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person30.html\">Andrei Arusoaie<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">15:10<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person287.html\">Radu Iosif<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Local Reasoning about Parameterized Reconfigurable Distributed Systems\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:186051\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">16:20-17:00<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 14: FROM Session (2)<\/span><\/div>\n<div style=\"border-left: 1px solid #cccccc; border-right: 1px solid #cccccc; border-bottom: 1px solid #cccccc; margin: 0pt 0pt 3pt; padding: 3pt 3pt 3pt 5pt; background: #add8db; border-radius: 0px 0px 6px 6px; color: #666666;\">\n<p style=\"margin-top: 0pt; margin-bottom: 0pt;\">Working Formal Methods Symposium<\/p>\n\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person42.html\">Florin Craciun<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">16:20<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person272.html\">Ioana Leu\u0219tean<\/a>\u00a0and\u00a0<a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person273.html\">Bogdan Macovei<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">DELP: Dynamic Epistemic Logic for Security Protocols\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:185999\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">16:40<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person275.html\">Alexandru-Ioan Lungu<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Alk Compound Data Types Translation in Z3\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-08.html#talk:185998\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\n<div style=\"text-align: center; padding: 5pt 0pt; font-size: 16px; margin: 4pt 0pt; background-color: #7a8687; font-style: normal; font-weight: 400;\">Thursday, December 9th<\/div>\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"font-size: 12pt; color: #666666; font-weight: bold;\">14:00-14:50<\/span><span style=\"font-size: 12pt;\">\u00a0<\/span><span style=\"font-size: 12pt; margin-left: 16pt;\">Session 18B: FROM Invited Talk (4)<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person70.html\">Laurentiu Leustean<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">14:00<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person290.html\">Florin Stoican<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">On the use of spline functions in motion planning\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-09.html#talk:186053\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"font-size: 12pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">15:10-16:00<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 19: FROM Invited Talk (5)<\/span><\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; font-size: 16px; font-style: normal; font-weight: 400;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person72.html\">Dorel Lucanu<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; font-size: 16px; font-style: normal; font-weight: 400;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400; width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">15:10<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person291.html\">Andrei Popescu<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Types-to-Sets for Theorem Proving in Higher-Order Logic\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-09.html#talk:186052\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"font-size: 13pt; background-color: #31d3e0; padding: 4pt 5pt 3pt; margin: 3pt 0pt 1pt; color: #555555;\"><span style=\"color: #666666; font-weight: bold;\">16:20-17:00<\/span>\u00a0<span style=\"margin-left: 16pt;\">Session 21: FROM Session (3) + Round Table<\/span><\/div>\n<div style=\"border-left: 1px solid #cccccc; border-right: 1px solid #cccccc; border-bottom: 1px solid #cccccc; margin: 0pt 0pt 3pt; padding: 3pt 3pt 3pt 5pt; background: #add8db; border-radius: 0px 0px 6px 6px; color: #666666; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\">\n<p style=\"margin-top: 0pt; margin-bottom: 0pt;\">Working Formal Methods Symposium<\/p>\n\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\">\n<div style=\"text-transform: uppercase; padding-right: 5pt; display: inline-block; vertical-align: top;\">CHAIR:<\/div>\n<div style=\"display: inline-block;\"><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person70.html\">Laurentiu Leustean<\/a><\/div>\n<\/div>\n<div style=\"margin: 2pt 0pt 2pt 5pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; text-decoration-thickness: initial; text-decoration-style: initial; text-decoration-color: initial;\"><span style=\"text-transform: uppercase; padding-right: 5pt;\">LOCATION:\u00a0<\/span><a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/room278.html\">Room FROM<\/a><\/div>\n<table style=\"margin: 2pt 0pt 2pt 20pt; color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;width:97.5%;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style = \"width: 5%\">16:20<\/td>\n<td style = \"width: 95%\">\n<div><a style=\"font-style: italic;  ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/person270.html\">Ana Iova<\/a><\/div>\n<div style=\"padding: 1pt 0pt; font-weight: bold;\">Software Testing Using Formal Methods\u00a0<span style=\"font-weight: normal; white-space: nowrap;\">(<a style=\" ;\" href=\"https:\/\/easychair.org\/smart-program\/SYNASC2021\/2021-12-09.html#talk:185968\">abstract<\/a>)<\/span><\/div><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\n<div style=\"color: #000000; font-family: Arial, Helvetica, sans-serif; font-size: 16px; font-style: normal; font-weight: 400;\"><\/div>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-5235aef elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"5235aef\" 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-fec476a\" data-id=\"fec476a\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-2f7f261 elementor-widget elementor-widget-heading\" data-id=\"2f7f261\" data-element_type=\"widget\" id=\"venue\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Venue <\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-4394247 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"4394247\" 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-33 elementor-top-column elementor-element elementor-element-c69372b\" data-id=\"c69372b\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-f4c5c73 elementor-widget elementor-widget-text-editor\" data-id=\"f4c5c73\" 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<p><strong style=\"font-size: 16px; color: #212529; font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto, 'Helvetica Neue', Arial, 'Noto Sans', sans-serif, 'Apple Color Emoji', 'Segoe UI Emoji', 'Segoe UI Symbol', 'Noto Color Emoji';\">Universitatea de Vest din Timi\u0219oara<\/strong><\/p><p>Bulevardul Vasile P\u00e2rvan 4, Timi\u0219oara 300223<\/p><h4 style=\"font-style: normal;\"><a href=\"https:\/\/synasc.ro\/2021\/travel-arrangements\/\" target=\"_blank\" rel=\"noopener\"><span style=\"font-size: 18px; text-decoration-line: underline;\">Travel arrangements<\/span><\/a><\/h4><h4><span style=\"text-decoration: underline;\"><a href=\"https:\/\/synasc.ro\/2021\/accommodation\/\" target=\"_blank\" rel=\"noopener\">Accommodation<\/a><\/span><\/h4><p>\u00a0<\/p><p>\u00a0<\/p><p>\u00a0<\/p>\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<div class=\"elementor-column elementor-col-66 elementor-top-column elementor-element elementor-element-b48a9a6\" data-id=\"b48a9a6\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-0cb330e elementor-widget elementor-widget-text-editor\" data-id=\"0cb330e\" 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<iframe src=\"https:\/\/www.google.com\/maps\/embed?pb=!1m14!1m8!1m3!1d22273.787246658772!2d21.22981!3d45.746667!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x47455d8484e124e5%3A0x5b3d17fa281f3902!2sBulevardul%20Vasile%20P%C3%A2rvan%204%2C%20Timi%C8%99oara%20300222%2C%20Romania!5e0!3m2!1sen!2sus!4v1628089436011!5m2!1sen!2sus\" width=\"600\" height=\"450\" style=\"border:0;\" allowfullscreen=\"\" loading=\"lazy\"><\/iframe>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-2c742fe elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"2c742fe\" 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-3dc4e0f\" data-id=\"3dc4e0f\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap\">\n\t\t\t\t\t\t\t\t\t<\/div>\n\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-2edd706 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"2edd706\" 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-e80485e\" data-id=\"e80485e\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-ad41e3d elementor-widget elementor-widget-heading\" data-id=\"ad41e3d\" data-element_type=\"widget\" id=\"organisers\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\"><br><br>Organisers <br><\/h2>\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t<section class=\"elementor-section elementor-top-section elementor-element elementor-element-d39341b elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"d39341b\" 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-25 elementor-top-column elementor-element elementor-element-4da2172\" data-id=\"4da2172\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-43ee2cf elementor-widget elementor-widget-image\" data-id=\"43ee2cf\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"318\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-1024x318.jpg\" class=\"attachment-large size-large\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-1024x318.jpg 1024w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-300x93.jpg 300w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-768x238.jpg 768w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-1536x476.jpg 1536w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-2048x635.jpg 2048w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/fmilogo-600x186.jpg 600w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/>\t\t\t\t\t\t\t\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<div class=\"elementor-column elementor-col-25 elementor-top-column elementor-element elementor-element-95469d1\" data-id=\"95469d1\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-14be2c6 elementor-widget elementor-widget-image\" data-id=\"14be2c6\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img loading=\"lazy\" decoding=\"async\" width=\"298\" height=\"300\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/ubb_FMI_logo-298x300.png\" class=\"attachment-medium size-medium\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/ubb_FMI_logo-298x300.png 298w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/ubb_FMI_logo-150x150.png 150w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/ubb_FMI_logo-100x100.png 100w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/ubb_FMI_logo.png 599w\" sizes=\"auto, (max-width: 298px) 100vw, 298px\" \/>\t\t\t\t\t\t\t\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<div class=\"elementor-column elementor-col-25 elementor-top-column elementor-element elementor-element-9ee9c8c\" data-id=\"9ee9c8c\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-66693ab elementor-widget elementor-widget-image\" data-id=\"66693ab\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img loading=\"lazy\" decoding=\"async\" width=\"381\" height=\"110\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/compsci_iasi_logo.png\" class=\"attachment-large size-large\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/compsci_iasi_logo.png 381w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/compsci_iasi_logo-300x87.png 300w\" sizes=\"auto, (max-width: 381px) 100vw, 381px\" \/>\t\t\t\t\t\t\t\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<div class=\"elementor-column elementor-col-25 elementor-top-column elementor-element elementor-element-4063df9\" data-id=\"4063df9\" data-element_type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t\t\t<div class=\"elementor-element elementor-element-86c1c92 elementor-widget elementor-widget-image\" data-id=\"86c1c92\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"1024\" src=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-1024x1024.png\" class=\"attachment-large size-large\" alt=\"\" srcset=\"https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1.png 1024w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-300x300.png 300w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-150x150.png 150w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-768x768.png 768w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-600x600.png 600w, https:\/\/from2021.cs.unibuc.ro\/wp-content\/uploads\/2021\/08\/uvt_fmi-1-100x100.png 100w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/>\t\t\t\t\t\t\t\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\t\t<\/div>\n\t\t<\/section>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>WORKING FORMAL METHODS SYMPOSIUMDecember 8-9, 2021, Timi\u0219oara, Romania In conjunction with SYNASC 2021 Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and\/or make the formal methods to work by creating or using software tools that apply theoretical &hellip;<\/p>\n<p class=\"read-more\"> <a class=\"\" href=\"https:\/\/from2021.cs.unibuc.ro\/\"> <span class=\"screen-reader-text\">One Page Website<\/span> Read More &raquo;<\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-303","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/pages\/303","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=303"}],"version-history":[{"count":480,"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/pages\/303\/revisions"}],"predecessor-version":[{"id":902,"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=\/wp\/v2\/pages\/303\/revisions\/902"}],"wp:attachment":[{"href":"https:\/\/from2021.cs.unibuc.ro\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=303"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}