{"id":2483,"date":"2020-05-29T10:19:16","date_gmt":"2020-05-29T08:19:16","guid":{"rendered":"http:\/\/synasc.ro\/2020\/?page_id=2483"},"modified":"2020-08-19T13:48:43","modified_gmt":"2020-08-19T11:48:43","slug":"ioana-leustean","status":"publish","type":"page","link":"http:\/\/synasc.ro\/2020\/ioana-leustean\/","title":{"rendered":"Ioana Leu\u0219tean"},"content":{"rendered":"\n<h2 class=\"has-text-align-center wp-block-heading\"><a href=\"https:\/\/cs.unibuc.ro\/\/~ileustean\/\">Ioana Leu\u0219tean<\/a><strong><br><\/strong><\/h2>\n\n\n\n<h2 class=\"has-text-align-center wp-block-heading\"> University of Bucharest, Romania <\/h2>\n\n\n\n<p class=\"has-text-align-center\"><strong>Abstract:<\/strong><\/p>\n\n\n\n<p><strong>Operational Semantics and Program Verification using Many-sorted Hybrid Modal Logic&nbsp;<\/strong><\/p>\n\n\n\n<p>In this talk we present the&nbsp;<em>many-sorted hybrid modal logic<\/em>, a logical system that is powerful enough to represent both the programs and their semantics in a uniform way.&nbsp;&nbsp;This logic is built by performing hybridization on top of a general many-sorted polyadic modal logic. Given a propositional modal logic, its hybrid companion is defined by adding nominals, atomic symbols that name the states of a model, as well as special operators and binders. The many-sorted hybrid modal logic is a sound and complete system with the property that, once a language is specified, one can define its operational semantics and perform Hoare-style verification.&nbsp;&nbsp;The SMC-inspired operational semantics is defined by a set of axioms derived from those of Propositional Dynamic Logic, and general Hoare-like assertions can be proved in this setting. We present our approach from general to particular, as well as challenges and future work.&nbsp;&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Ioana Leu\u0219tean University of Bucharest, Romania Abstract: Operational Semantics and Program Verification using Many-sorted Hybrid Modal Logic&nbsp; In this talk we present the&nbsp;many-sorted hybrid modal logic, a logical system that is powerful enough to represent both the programs and their semantics in a uniform way.&nbsp;&nbsp;This logic is built by performing hybridization on top of a [&hellip;]<\/p>\n","protected":false},"author":23,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-2483","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/pages\/2483","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/users\/23"}],"replies":[{"embeddable":true,"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/comments?post=2483"}],"version-history":[{"count":2,"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/pages\/2483\/revisions"}],"predecessor-version":[{"id":2641,"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/pages\/2483\/revisions\/2641"}],"wp:attachment":[{"href":"http:\/\/synasc.ro\/2020\/wp-json\/wp\/v2\/media?parent=2483"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}