Probabilistic Programming: A True Verification Challenge

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    109 Downloads (Pure)


    Probabilistic programs [6] are sequential programs, written in languages like C, Java, Scala, or ML, with two added constructs: (1) the ability to draw values at random from probability distributions, and (2) the ability to condition values of variables in a program through observations. For a comprehensive treatment, see [3]. They have a wide range of applications. Probabilistic programming is at the heart of machine learning for describing distribution functions; Bayesian inference is pivotal in their analysis. Probabilistic programs are central in security for describing cryptographic constructions (such as randomised encryption) and security experiments. In addition, probabilistic programs are an active research topic in quantitative information flow. Quantum programs are inherently probabilistic due to the random outcomes of quantum measurements. Finally, probabilistic programs can be used for approximate computing, e.g., by specifying reliability requirements for programs that allocate data in unreliable memory and use unreliable operations in hardware (so as to save energy dissipation) [1]. Other applications include [4] scientific modeling, information retrieval, bio–informatics, epidemiology, vision, seismic analysis, semantic web, business intelligence, human cognition, and more. Microsoft has started an initiative to improve the usability of probabilistic programming which has resulted in languages such as R2 [13] and Tabular [5] emerged.
    Original languageEnglish
    Title of host publicationAutomated Technology for Verification and Analysis
    Subtitle of host publication13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings
    EditorsBernd Finkbeiner, Geguang Pu, Lijun Zhang
    Place of PublicationLondon
    Number of pages3
    ISBN (Electronic)978-3-319-24953-
    ISBN (Print)978-3-319-24953-7
    Publication statusPublished - Oct 2015
    Event13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015 - Shanghai, China, Shanghai, China
    Duration: 12 Oct 201515 Oct 2015
    Conference number: 13

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
    Abbreviated titleATVA
    Other12-15 October 2015
    Internet address


    • EWI-26665
    • METIS-315145
    • IR-98974


    Dive into the research topics of 'Probabilistic Programming: A True Verification Challenge'. Together they form a unique fingerprint.

    Cite this