{"id":12251,"date":"2022-01-26T14:48:15","date_gmt":"2022-01-26T14:48:15","guid":{"rendered":"https:\/\/direc.dk\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/"},"modified":"2025-10-20T13:14:25","modified_gmt":"2025-10-20T13:14:25","slug":"automated-verification-of-sensitivity-properties-for-probabilistic-programs","status":"publish","type":"post","link":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/","title":{"rendered":"Automated Verification of Sensitivity Properties for Probabilistic Programs"},"content":{"rendered":"\t\t<div data-elementor-type=\"wp-post\" data-elementor-id=\"12251\" class=\"elementor elementor-12251 elementor-12065\" data-elementor-post-type=\"post\">\n\t\t\t\t\t\t<section data-particle_enable=\"false\" data-particle-mobile-disabled=\"false\" class=\"elementor-section elementor-top-section elementor-element elementor-element-7c5836f8 elementor-section-height-min-height elementor-section-items-stretch elementor-section-content-middle elementor-reverse-mobile elementor-reverse-tablet elementor-section-full_width elementor-section-height-default\" data-id=\"7c5836f8\" data-element_type=\"section\" data-e-type=\"section\" data-settings=\"{&quot;background_background&quot;:&quot;classic&quot;,&quot;shape_divider_bottom&quot;:&quot;triangle&quot;,&quot;shape_divider_bottom_negative&quot;:&quot;yes&quot;,&quot;jet_parallax_layout_list&quot;:[]}\">\n\t\t\t\t\t\t\t<div class=\"elementor-background-overlay\"><\/div>\n\t\t\t\t\t\t<div class=\"elementor-shape elementor-shape-bottom\" aria-hidden=\"true\" data-negative=\"true\">\n\t\t\t<svg xmlns=\"http:\/\/www.w3.org\/2000\/svg\" viewBox=\"0 0 1000 100\" preserveAspectRatio=\"none\">\n\t<path class=\"elementor-shape-fill\" d=\"M500.2,94.7L0,0v100h1000V0L500.2,94.7z\"\/>\n<\/svg>\t\t<\/div>\n\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-no\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-31ee6a3d\" data-id=\"31ee6a3d\" data-element_type=\"column\" data-e-type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap elementor-element-populated\">\n\t\t\t\t\t\t<section data-particle_enable=\"false\" data-particle-mobile-disabled=\"false\" class=\"elementor-section elementor-inner-section elementor-element elementor-element-386f5fc2 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"386f5fc2\" data-element_type=\"section\" data-e-type=\"section\" data-settings=\"{&quot;jet_parallax_layout_list&quot;:[]}\">\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-50 elementor-inner-column elementor-element elementor-element-2d565a20\" data-id=\"2d565a20\" data-element_type=\"column\" data-e-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-47cbc803 elementor-widget elementor-widget-heading\" data-id=\"47cbc803\" data-element_type=\"widget\" data-e-type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<h2 class=\"elementor-heading-title elementor-size-default\">DIREC-projekt<\/h2>\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-722b2a77 animated-fast elementor-invisible elementor-widget elementor-widget-heading\" data-id=\"722b2a77\" data-element_type=\"widget\" data-e-type=\"widget\" data-settings=\"{&quot;_animation&quot;:&quot;fadeIn&quot;}\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<h1 class=\"elementor-heading-title elementor-size-default\">Automated Verification of Sensitivity Properties for Probabilistic Programs<\/h1>\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-50 elementor-inner-column elementor-element elementor-element-6f670271\" data-id=\"6f670271\" data-element_type=\"column\" data-e-type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap\">\n\t\t\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<section data-particle_enable=\"false\" data-particle-mobile-disabled=\"false\" class=\"elementor-section elementor-top-section elementor-element elementor-element-7f5f5830 elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"7f5f5830\" data-element_type=\"section\" data-e-type=\"section\" data-settings=\"{&quot;background_background&quot;:&quot;classic&quot;,&quot;jet_parallax_layout_list&quot;:[]}\">\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-50 elementor-top-column elementor-element elementor-element-142ef72\" data-id=\"142ef72\" data-element_type=\"column\" data-e-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-27453b8c elementor-widget elementor-widget-heading\" data-id=\"27453b8c\" data-element_type=\"widget\" data-e-type=\"widget\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<h4 class=\"elementor-heading-title elementor-size-default\">Resum\u00e9<\/h4>\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-50 elementor-top-column elementor-element elementor-element-63ce34b8\" data-id=\"63ce34b8\" data-element_type=\"column\" data-e-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-5426b5b6 elementor-widget elementor-widget-text-editor\" data-id=\"5426b5b6\" data-element_type=\"widget\" data-e-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>Sensitivitet beskriver, hvordan programudgange \u00e6ndrer sig, n\u00e5r input \u00e6ndres. Vi foresl\u00e5r at unders\u00f8ge nye metoder til at specificere og verificere sensitivitetsegenskaber for probabilistiske programmer, s\u00e5 de (a) er lette at forst\u00e5 for almindelige programm\u00f8rer, (b) kan verificeres med automatiserede teorembevisere, og (c) omfatter egenskaber fra maskinl\u00e6ring og sikkerhedslitteraturen.<\/p>\n<p><strong>Projektperiode:<\/strong> 2022-2023<\/p>\n<p><strong>Projektleder<\/strong><\/p>\n<ul>\n<li>Associate Professor Christoph Matheja<\/li>\n<li>Department of Applied Mathematics and Computer Science, DTU<\/li>\n<li>chmat@dtu.dk<\/li>\n<\/ul>\n<p>og<\/p>\n<ul>\n<li>Postdoc Alejandro Aguirre<\/li>\n<li>Department of Computer Science, AU<\/li>\n<li>alejandro@cs.au.dk<\/li>\n<\/ul>\n\t\t\t\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t<div class=\"elementor-element elementor-element-d223e06 elementor-widget elementor-widget-toggle\" data-id=\"d223e06\" data-element_type=\"widget\" data-e-type=\"widget\" data-settings=\"{&quot;_animation&quot;:&quot;none&quot;}\" data-widget_type=\"toggle.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t\t\t<div class=\"elementor-toggle\">\n\t\t\t\t\t\t\t<div class=\"elementor-toggle-item\">\n\t\t\t\t\t<div id=\"elementor-tab-title-2201\" class=\"elementor-tab-title\" data-tab=\"1\" role=\"button\" aria-controls=\"elementor-tab-content-2201\" aria-expanded=\"false\">\n\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon elementor-toggle-icon-left\" aria-hidden=\"true\">\n\t\t\t\t\t\t\t\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-closed\"><i class=\"fas fa-caret-right\"><\/i><\/span>\n\t\t\t\t\t\t\t\t<span class=\"elementor-toggle-icon-opened\"><i class=\"elementor-toggle-icon-opened fas fa-caret-up\"><\/i><\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t\t<\/span>\n\t\t\t\t\t\t\t\t\t\t\t\t<a class=\"elementor-toggle-title\" tabindex=\"0\">Mere om projektet (p\u00e5 engelsk)<\/a>\n\t\t\t\t\t<\/div>\n\n\t\t\t\t\t<div id=\"elementor-tab-content-2201\" class=\"elementor-tab-content elementor-clearfix\" data-tab=\"1\" role=\"region\" aria-labelledby=\"elementor-tab-title-2201\"><p>Our overall objective is to explore how automated verification of sensitivity properties of probabilistic programs can support developers in increasing the trust in their software through formal assurances.<\/p>\n<p>Probabilistic programs are programs with the ability to sample from probability distributions. Examples include randomized algorithms, where sampling is exploited to ensure that expensive executions have a low probability, cryptographic protocols, where randomness is essential for encoding secrets, and statistics, where programs are becoming a popular alternative to graphical models for describing complex distributions.<\/p>\n<p>The sensitivity of a program determines how its outputs are affected by changes to its input; programs with low sensitivity are robust against fluctuations in their input \u2013 a key property for improving trust in software. Minor input changes should, for example, not affect the result of a classifier learned from training data. In the probabilistic setting, the output of a program depends not only on the input but also on the source of randomness. Hence, the notion of sensitivity \u2013 as well as techniques for reasoning about it \u2013 needs refinement.<\/p>\n<p>Automated verification takes a deductive approach to proving that a program satisfies its specification: users annotate their programs with logical assertions; a verifier then generates verification conditions (VCs) whose validity implies that the program\u2019s specification holds. Deductive verifiers are more complete and more scalable than fully automatic techniques but require significant user interaction. The main challenge for users of automated verifiers lies in finding suitable intermediate assertions, particularly loop invariants, such that an automated theorem prover can discharge the generated VCs. A significant challenge for developers of automated verifiers is to keep the amount and complexity of necessary annotations as low as possible.<\/p>\n<p>Previous work [1] co-authored by the applicants provides a theoretical framework for reasoning about the sensitivity of probabilistic programs: the above paper presents a calculus to carry out \u201cpen-and-paper\u201d proofs of sensitivity in a principled and syntax-directed manner. The proposed technique deals with sampling instructions by requiring users to identify suitable probabilistic couplings, which act as synchronization points, on top of finding loop invariants. However, the technique is limited in the sense that it does not provide tight sensitivity bounds when changes to the input cause a program to take a different branch on a conditional.<\/p>\n<p>Our project has four main goals. First, we will develop methodologies that do not suffer from the limitations of [1]. We believe that conditional branching can be treated by carefully tracking the possible divergence.<\/p>\n<p>Second, we will develop an automated verification tool for proving sensitivity properties of probabilistic programs. The tool will generate VCs based on the calculus from [1], which will be discharged using an SMT solver. In designing the specification language, we aim to achieve a balance so that (a) users can conveniently specify synchronization points for random samples (via so-called probabilistic couplings) and (b) existing solvers can prove the resulting VCs.<\/p>\n<p>Third, we aim to aid the verification process by assisting users in finding synchronization points. Invariant synthesis has been extensively studied in the case of deterministic programs. Similarly, coupling synthesis has been recently studied for the verification of probabilistic programs. We believe these techniques can be adapted to the study of sensitivity.<\/p>\n<p>Finally, we will validate the overall verification system by applying it to case studies from machine learning, statistics, and randomized algorithms.<\/p>\n<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t\t<\/div>\n\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<section data-particle_enable=\"false\" data-particle-mobile-disabled=\"false\" class=\"elementor-section elementor-top-section elementor-element elementor-element-590f9a10 elementor-section-height-min-height elementor-section-items-stretch elementor-section-content-middle elementor-reverse-mobile elementor-reverse-tablet elementor-section-stretched elementor-section-boxed elementor-section-height-default\" data-id=\"590f9a10\" data-element_type=\"section\" data-e-type=\"section\" data-settings=\"{&quot;stretch_section&quot;:&quot;section-stretched&quot;,&quot;jet_parallax_layout_list&quot;:[]}\">\n\t\t\t\t\t\t<div class=\"elementor-container elementor-column-gap-no\">\n\t\t\t\t\t<div class=\"elementor-column elementor-col-100 elementor-top-column elementor-element elementor-element-4e05d574\" data-id=\"4e05d574\" data-element_type=\"column\" data-e-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<div class=\"elementor-background-overlay\"><\/div>\n\t\t\t\t\t\t<div class=\"elementor-element elementor-element-62b80499 animated-fast elementor-invisible elementor-widget elementor-widget-heading\" data-id=\"62b80499\" data-element_type=\"widget\" data-e-type=\"widget\" data-settings=\"{&quot;_animation&quot;:&quot;fadeIn&quot;}\" data-widget_type=\"heading.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<h3 class=\"elementor-heading-title elementor-size-default\">Insights<\/h3>\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<section data-particle_enable=\"false\" data-particle-mobile-disabled=\"false\" class=\"elementor-section elementor-top-section elementor-element elementor-element-59069d99 elementor-section-stretched elementor-section-boxed elementor-section-height-default elementor-section-height-default\" data-id=\"59069d99\" data-element_type=\"section\" data-e-type=\"section\" data-settings=\"{&quot;stretch_section&quot;:&quot;section-stretched&quot;,&quot;jet_parallax_layout_list&quot;:[]}\">\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-50 elementor-top-column elementor-element elementor-element-16ad3b14\" data-id=\"16ad3b14\" data-element_type=\"column\" data-e-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-5f9bc8b7 elementor-widget__width-initial elementor-widget elementor-widget-eael-post-list\" data-id=\"5f9bc8b7\" data-element_type=\"widget\" data-e-type=\"widget\" data-widget_type=\"eael-post-list.default\">\n\t\t\t\t<div class=\"elementor-widget-container\">\n\t\t\t\t\t<div class=\"eael-post-list-container default layout-default\"><div class=\"eael-post-list-wrap\"><div class=\"eael-post-list-posts-wrap eael-post-appender eael-post-appender-5f9bc8b7\"><div class=\"eael-post-list-post \"><div class=\"eael-post-list-thumbnail \"><a href=\"https:\/\/direc.dk\/da\/automated-sensitivity-analysis-enhances-trustworthiness-of-probabilistic-programs\/\">\n                            <img decoding=\"async\" src=\"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news-1024x576.png\" alt=\"\">\n                        <\/a><\/div><div class=\"eael-post-list-content\"><h2 class=\"eael-post-list-title\"><a href=\"https:\/\/direc.dk\/da\/automated-sensitivity-analysis-enhances-trustworthiness-of-probabilistic-programs\/\" >Automatiseret f\u00f8lsomhedsanalyse forbedrer p\u00e5lideligheden af sandsynlighedsprogrammer.<\/a><\/h2><div class=\"meta\"><span class=\"eael-post-published-date\"><i class=\"far fa-calendar-alt\"><\/i> 6. marts 2024<\/span><\/div><\/div><\/div><\/div><\/div>\n\t\t<\/div>\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-50 elementor-top-column elementor-element elementor-element-9d3249b\" data-id=\"9d3249b\" data-element_type=\"column\" data-e-type=\"column\">\n\t\t\t<div class=\"elementor-widget-wrap\">\n\t\t\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>Vores overordnede m\u00e5l er at unders\u00f8ge, hvordan automatiseret verifikation af sensitivitetsegenskaber i probabilistiske programmer kan hj\u00e6lpe udviklere med at \u00f8ge tilliden til deres software gennem formelle garantier.<\/p>\n","protected":false},"author":3,"featured_media":28153,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[188,212,33,218],"tags":[],"class_list":["post-12251","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-afsluttet-projekt","category-dataanalyse-og-algoritmer","category-explore-projekt","category-projekt"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v28.1 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC<\/title>\n<meta name=\"description\" content=\"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.\" \/>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/\" \/>\n<meta property=\"og:locale\" content=\"da_DK\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC\" \/>\n<meta property=\"og:description\" content=\"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.\" \/>\n<meta property=\"og:url\" content=\"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/\" \/>\n<meta property=\"og:site_name\" content=\"DIREC\" \/>\n<meta property=\"article:published_time\" content=\"2022-01-26T14:48:15+00:00\" \/>\n<meta property=\"article:modified_time\" content=\"2025-10-20T13:14:25+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png\" \/>\n\t<meta property=\"og:image:width\" content=\"1920\" \/>\n\t<meta property=\"og:image:height\" content=\"1080\" \/>\n\t<meta property=\"og:image:type\" content=\"image\/png\" \/>\n<meta name=\"author\" content=\"Susanne Br\u00f8ndberg\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Skrevet af\" \/>\n\t<meta name=\"twitter:data1\" content=\"Susanne Br\u00f8ndberg\" \/>\n\t<meta name=\"twitter:label2\" content=\"Estimeret l\u00e6setid\" \/>\n\t<meta name=\"twitter:data2\" content=\"4 minutter\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\\\/\\\/schema.org\",\"@graph\":[{\"@type\":\"Article\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#article\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/\"},\"author\":{\"name\":\"Susanne Br\u00f8ndberg\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#\\\/schema\\\/person\\\/3fcdff2b9bc83fcb7b642fa67a946f38\"},\"headline\":\"Automated Verification of Sensitivity Properties for Probabilistic Programs\",\"datePublished\":\"2022-01-26T14:48:15+00:00\",\"dateModified\":\"2025-10-20T13:14:25+00:00\",\"mainEntityOfPage\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/\"},\"wordCount\":662,\"publisher\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#organization\"},\"image\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2024\\\/03\\\/Probabilistic-Programs_news.png\",\"articleSection\":[\"Afsluttet projekt\",\"Dataanalyse og algoritmer\",\"Explore-projekt\",\"Projekt\"],\"inLanguage\":\"da-DK\"},{\"@type\":\"WebPage\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/\",\"url\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/\",\"name\":\"Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC\",\"isPartOf\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#website\"},\"primaryImageOfPage\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#primaryimage\"},\"image\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#primaryimage\"},\"thumbnailUrl\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2024\\\/03\\\/Probabilistic-Programs_news.png\",\"datePublished\":\"2022-01-26T14:48:15+00:00\",\"dateModified\":\"2025-10-20T13:14:25+00:00\",\"description\":\"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.\",\"breadcrumb\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#breadcrumb\"},\"inLanguage\":\"da-DK\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/\"]}]},{\"@type\":\"ImageObject\",\"inLanguage\":\"da-DK\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#primaryimage\",\"url\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2024\\\/03\\\/Probabilistic-Programs_news.png\",\"contentUrl\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2024\\\/03\\\/Probabilistic-Programs_news.png\",\"width\":1920,\"height\":1080},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\\\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Home\",\"item\":\"https:\\\/\\\/direc.dk\\\/da\\\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Automated Verification of Sensitivity Properties for Probabilistic Programs\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#website\",\"url\":\"https:\\\/\\\/direc.dk\\\/da\\\/\",\"name\":\"DIREC\",\"description\":\"Digital Research Centre Denmark\",\"publisher\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\\\/\\\/direc.dk\\\/da\\\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"da-DK\"},{\"@type\":\"Organization\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#organization\",\"name\":\"DIREC\",\"url\":\"https:\\\/\\\/direc.dk\\\/da\\\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"da-DK\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#\\\/schema\\\/logo\\\/image\\\/\",\"url\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2021\\\/02\\\/DIREC_logo_2023_bla.png\",\"contentUrl\":\"https:\\\/\\\/direc.dk\\\/wp-content\\\/uploads\\\/2021\\\/02\\\/DIREC_logo_2023_bla.png\",\"width\":2786,\"height\":786,\"caption\":\"DIREC\"},\"image\":{\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#\\\/schema\\\/logo\\\/image\\\/\"}},{\"@type\":\"Person\",\"@id\":\"https:\\\/\\\/direc.dk\\\/da\\\/#\\\/schema\\\/person\\\/3fcdff2b9bc83fcb7b642fa67a946f38\",\"name\":\"Susanne Br\u00f8ndberg\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"da-DK\",\"@id\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g\",\"url\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g\",\"contentUrl\":\"https:\\\/\\\/secure.gravatar.com\\\/avatar\\\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g\",\"caption\":\"Susanne Br\u00f8ndberg\"},\"url\":\"https:\\\/\\\/direc.dk\\\/da\\\/author\\\/susanne\\\/\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC","description":"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.","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:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/","og_locale":"da_DK","og_type":"article","og_title":"Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC","og_description":"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.","og_url":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/","og_site_name":"DIREC","article_published_time":"2022-01-26T14:48:15+00:00","article_modified_time":"2025-10-20T13:14:25+00:00","og_image":[{"width":1920,"height":1080,"url":"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png","type":"image\/png"}],"author":"Susanne Br\u00f8ndberg","twitter_card":"summary_large_image","twitter_misc":{"Skrevet af":"Susanne Br\u00f8ndberg","Estimeret l\u00e6setid":"4 minutter"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"Article","@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#article","isPartOf":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/"},"author":{"name":"Susanne Br\u00f8ndberg","@id":"https:\/\/direc.dk\/da\/#\/schema\/person\/3fcdff2b9bc83fcb7b642fa67a946f38"},"headline":"Automated Verification of Sensitivity Properties for Probabilistic Programs","datePublished":"2022-01-26T14:48:15+00:00","dateModified":"2025-10-20T13:14:25+00:00","mainEntityOfPage":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/"},"wordCount":662,"publisher":{"@id":"https:\/\/direc.dk\/da\/#organization"},"image":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#primaryimage"},"thumbnailUrl":"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png","articleSection":["Afsluttet projekt","Dataanalyse og algoritmer","Explore-projekt","Projekt"],"inLanguage":"da-DK"},{"@type":"WebPage","@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/","url":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/","name":"Automated Verification of Sensitivity Properties for Probabilistic Programs - DIREC","isPartOf":{"@id":"https:\/\/direc.dk\/da\/#website"},"primaryImageOfPage":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#primaryimage"},"image":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#primaryimage"},"thumbnailUrl":"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png","datePublished":"2022-01-26T14:48:15+00:00","dateModified":"2025-10-20T13:14:25+00:00","description":"Artificial Intelligence brings the promise of technological means to solve problems that previously were assumed to require human intelligence, and ultimately provide human-centered solutions that are both more effective and of higher quality in a synergy between the human and the AI system than solutions that are provided by humans or by an AI system alone.","breadcrumb":{"@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#breadcrumb"},"inLanguage":"da-DK","potentialAction":[{"@type":"ReadAction","target":["https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/"]}]},{"@type":"ImageObject","inLanguage":"da-DK","@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#primaryimage","url":"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png","contentUrl":"https:\/\/direc.dk\/wp-content\/uploads\/2024\/03\/Probabilistic-Programs_news.png","width":1920,"height":1080},{"@type":"BreadcrumbList","@id":"https:\/\/direc.dk\/da\/automated-verification-of-sensitivity-properties-for-probabilistic-programs\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Home","item":"https:\/\/direc.dk\/da\/"},{"@type":"ListItem","position":2,"name":"Automated Verification of Sensitivity Properties for Probabilistic Programs"}]},{"@type":"WebSite","@id":"https:\/\/direc.dk\/da\/#website","url":"https:\/\/direc.dk\/da\/","name":"DIREC","description":"Digital Research Centre Denmark","publisher":{"@id":"https:\/\/direc.dk\/da\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/direc.dk\/da\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"da-DK"},{"@type":"Organization","@id":"https:\/\/direc.dk\/da\/#organization","name":"DIREC","url":"https:\/\/direc.dk\/da\/","logo":{"@type":"ImageObject","inLanguage":"da-DK","@id":"https:\/\/direc.dk\/da\/#\/schema\/logo\/image\/","url":"https:\/\/direc.dk\/wp-content\/uploads\/2021\/02\/DIREC_logo_2023_bla.png","contentUrl":"https:\/\/direc.dk\/wp-content\/uploads\/2021\/02\/DIREC_logo_2023_bla.png","width":2786,"height":786,"caption":"DIREC"},"image":{"@id":"https:\/\/direc.dk\/da\/#\/schema\/logo\/image\/"}},{"@type":"Person","@id":"https:\/\/direc.dk\/da\/#\/schema\/person\/3fcdff2b9bc83fcb7b642fa67a946f38","name":"Susanne Br\u00f8ndberg","image":{"@type":"ImageObject","inLanguage":"da-DK","@id":"https:\/\/secure.gravatar.com\/avatar\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g","url":"https:\/\/secure.gravatar.com\/avatar\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g","contentUrl":"https:\/\/secure.gravatar.com\/avatar\/e8d2e418b1a0402f1ebb3e45dc93b7b681ec163ec692e71cb65c848ff80d3ab7?s=96&d=mm&r=g","caption":"Susanne Br\u00f8ndberg"},"url":"https:\/\/direc.dk\/da\/author\/susanne\/"}]}},"dynamic_page_title":"","dynamic_page_description":"","dynamic_page_partners":"","dynamic_page_scientific_impact":"","dynamic_page_people":"","dynamic_page_project_period":"","dynamic_page_funding":"","dynamic_page_publications":"","dynamic_page_cover_image":"","_links":{"self":[{"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/posts\/12251","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/comments?post=12251"}],"version-history":[{"count":3,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/posts\/12251\/revisions"}],"predecessor-version":[{"id":38271,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/posts\/12251\/revisions\/38271"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/media\/28153"}],"wp:attachment":[{"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/media?parent=12251"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/categories?post=12251"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/direc.dk\/da\/wp-json\/wp\/v2\/tags?post=12251"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}