{"id":457,"date":"2025-03-27T13:16:53","date_gmt":"2025-03-27T13:16:53","guid":{"rendered":"https:\/\/synasc.ro\/2025-new\/?page_id=457"},"modified":"2025-04-04T08:37:13","modified_gmt":"2025-04-04T08:37:13","slug":"thomas-henzinger","status":"publish","type":"page","link":"https:\/\/synasc.ro\/2025\/invited-speakers\/thomas-henzinger\/","title":{"rendered":"Thomas Henzinger"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-page\" data-elementor-id=\"457\" class=\"elementor elementor-457\" data-elementor-post-type=\"page\">\n\t\t\t\t<div class=\"elementor-element elementor-element-145994c e-con-full e-flex e-con e-parent\" data-id=\"145994c\" data-element_type=\"container\">\n\t\t\t\t<div class=\"elementor-element elementor-element-8629fff elementor-widget elementor-widget-heading\" data-id=\"8629fff\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Neural Certificates<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-09bd1b8 elementor-widget elementor-widget-heading\" data-id=\"09bd1b8\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">Thomas Henzinger<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-03b1c84 elementor-widget elementor-widget-text-editor\" data-id=\"03b1c84\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<p>Technical University of Vienna, Austria<\/p>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-b320374 elementor-widget elementor-widget-image\" data-id=\"b320374\" data-element_type=\"widget\" data-widget_type=\"image.default\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<img fetchpriority=\"high\" decoding=\"async\" width=\"216\" height=\"300\" src=\"https:\/\/synasc.ro\/2025\/wp-content\/uploads\/sites\/26\/2025\/03\/thomas_henzinger-216x300.jpeg\" class=\"attachment-medium size-medium wp-image-465\" alt=\"\" srcset=\"https:\/\/synasc.ro\/2025\/wp-content\/uploads\/sites\/26\/2025\/03\/thomas_henzinger-216x300.jpeg 216w, https:\/\/synasc.ro\/2025\/wp-content\/uploads\/sites\/26\/2025\/03\/thomas_henzinger.jpeg 470w\" sizes=\"(max-width: 216px) 100vw, 216px\" \/>\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-2f77387 elementor-align-center elementor-icon-list--layout-traditional elementor-list-item-link-full_width elementor-widget elementor-widget-icon-list\" data-id=\"2f77387\" data-element_type=\"widget\" data-widget_type=\"icon-list.default\">\n\t\t\t\t\t\t\t<ul class=\"elementor-icon-list-items\">\n\t\t\t\t\t\t\t<li class=\"elementor-icon-list-item\">\n\t\t\t\t\t\t\t\t\t\t\t<a href=\"https:\/\/pub.ista.ac.at\/~tah\/\">\n\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-icon\">\n\t\t\t\t\t\t\t<svg aria-hidden=\"true\" class=\"e-font-icon-svg e-fas-globe\" viewBox=\"0 0 496 512\" xmlns=\"http:\/\/www.w3.org\/2000\/svg\"><path d=\"M336.5 160C322 70.7 287.8 8 248 8s-74 62.7-88.5 152h177zM152 256c0 22.2 1.2 43.5 3.3 64h185.3c2.1-20.5 3.3-41.8 3.3-64s-1.2-43.5-3.3-64H155.3c-2.1 20.5-3.3 41.8-3.3 64zm324.7-96c-28.6-67.9-86.5-120.4-158-141.6 24.4 33.8 41.2 84.7 50 141.6h108zM177.2 18.4C105.8 39.6 47.8 92.1 19.3 160h108c8.7-56.9 25.5-107.8 49.9-141.6zM487.4 192H372.7c2.1 21 3.3 42.5 3.3 64s-1.2 43-3.3 64h114.6c5.5-20.5 8.6-41.8 8.6-64s-3.1-43.5-8.5-64zM120 256c0-21.5 1.2-43 3.3-64H8.6C3.2 212.5 0 233.8 0 256s3.2 43.5 8.6 64h114.6c-2-21-3.2-42.5-3.2-64zm39.5 96c14.5 89.3 48.7 152 88.5 152s74-62.7 88.5-152h-177zm159.3 141.6c71.4-21.2 129.4-73.7 158-141.6h-108c-8.8 56.9-25.6 107.8-50 141.6zM19.3 352c28.6 67.9 86.5 120.4 158 141.6-24.4-33.8-41.2-84.7-50-141.6h-108z\"><\/path><\/svg>\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-icon-list-text\">Webpage<\/span>\n\t\t\t\t\t\t\t\t\t\t\t<\/a>\n\t\t\t\t\t\t\t\t\t<\/li>\n\t\t\t\t\t\t<\/ul>\n\t\t\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-9460312 elementor-widget elementor-widget-heading\" data-id=\"9460312\" data-element_type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">ABSTRACT<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-03c398a elementor-widget elementor-widget-text-editor\" data-id=\"03c398a\" data-element_type=\"widget\" data-widget_type=\"text-editor.default\">\n\t\t\t\t\t\t\t\t\t<div dir=\"auto\">Symbolic datatypes are central to abstract reasoning about dynamical systems. Successful examples include BDDs and SAT for finite-state systems, and polyhedra and SMT for discrete dynamical systems over certain infinite state spaces. Neural networks provide a natural symbolic datatype over continuous state spaces, with the added benefit of supporting key operations while being trainable. We advocate using neural networks for multiple purposes in reasoning about continuous state spaces, particularly for representing both deterministic dynamics\u2014such as controllers\u2014and correctness certificates. A correctness certificate is a succinct witness for a desired property of a dynamical system. For example, invariants and barrier functions certify safety, while Lyapunov functions and supermartingales certify progress. Stochastic barrier functions and supermartingales can further account for uncertainty (noise) in system dynamics. Established techniques from machine learning and formal reasoning about neural networks\u2014such as SMT, abstract interpretation, and counterexample-guided refinement\u2014enable the joint synthesis of controllers and correctness certificates. This allows for the synthesis of guaranteed-to-be-correct controllers, where both the controllers and their certificates are represented, learned, and verified as neural networks. This talk includes joint work with Krishnendu Chatterjee, Mathias Lechner, and Djordje Zikelic.<\/div>\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t","protected":false},"excerpt":{"rendered":"<p>Neural Certificates Thomas Henzinger Technical University of Vienna, Austria Webpage ABSTRACT Symbolic datatypes are central to abstract reasoning about dynamical systems. Successful examples include BDDs and SAT for finite-state systems, and polyhedra and SMT for discrete dynamical systems over certain infinite state spaces. Neural networks provide a natural symbolic datatype over continuous state spaces, with [&hellip;]<\/p>\n","protected":false},"author":27,"featured_media":0,"parent":226,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-457","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/pages\/457","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/users\/27"}],"replies":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/comments?post=457"}],"version-history":[{"count":28,"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/pages\/457\/revisions"}],"predecessor-version":[{"id":885,"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/pages\/457\/revisions\/885"}],"up":[{"embeddable":true,"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/pages\/226"}],"wp:attachment":[{"href":"https:\/\/synasc.ro\/2025\/wp-json\/wp\/v2\/media?parent=457"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}