Probabilistic Programming: A True Verification Challenge

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

Abstract

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.
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
PublisherSpringer
Pages1-3
Number of pages3
ISBN (Electronic)978-3-319-24953-
ISBN (Print)978-3-319-24953-7
DOIs
StatePublished - 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
http://atva2015.ios.ac.cn/

Publication series

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

Conference

Conference13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015
Abbreviated titleATVA
CountryChina
CityShanghai
Period12/10/1515/10/15
Other12-15 October 2015
Internet address

Fingerprint

Competitive intelligence
Describing functions
Epidemiology
Bioinformatics
Semantic Web
Computer programming
Information retrieval
Probability distributions
Computer hardware
Cryptography
Distribution functions
Learning systems
Energy dissipation
Data storage equipment
Experiments

Keywords

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

Cite this

Katoen, J. P. (2015). Probabilistic Programming: A True Verification Challenge. In B. Finkbeiner, G. Pu, & L. Zhang (Eds.), Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings (pp. 1-3). (Lecture Notes in Computer Science; Vol. 9364). London: Springer. DOI: 10.1007/978-3-319-24953-7_1
Katoen, Joost P./ Probabilistic Programming : A True Verification Challenge. Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. editor / Bernd Finkbeiner ; Geguang Pu ; Lijun Zhang. London : Springer, 2015. pp. 1-3 (Lecture Notes in Computer Science).
@inproceedings{7f6aa514f3864dbfbdcaacd9b2556caf,
title = "Probabilistic Programming: A True Verification Challenge",
abstract = "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.",
keywords = "EWI-26665, METIS-315145, IR-98974",
author = "Katoen, {Joost P.}",
note = "10.1007/978-3-319-24953-7_1",
year = "2015",
month = "10",
doi = "10.1007/978-3-319-24953-7_1",
language = "English",
isbn = "978-3-319-24953-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--3",
editor = "Bernd Finkbeiner and Geguang Pu and Lijun Zhang",
booktitle = "Automated Technology for Verification and Analysis",

}

Katoen, JP 2015, Probabilistic Programming: A True Verification Challenge. in B Finkbeiner, G Pu & L Zhang (eds), Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9364, Springer, London, pp. 1-3, 13th International Symposium on Automated Technology for Verification and Analysis, ATVA 2015, Shanghai, China, 12/10/15. DOI: 10.1007/978-3-319-24953-7_1

Probabilistic Programming : A True Verification Challenge. / Katoen, Joost P.

Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. ed. / Bernd Finkbeiner; Geguang Pu; Lijun Zhang. London : Springer, 2015. p. 1-3 (Lecture Notes in Computer Science; Vol. 9364).

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

TY - GEN

T1 - Probabilistic Programming

T2 - A True Verification Challenge

AU - Katoen,Joost P.

N1 - 10.1007/978-3-319-24953-7_1

PY - 2015/10

Y1 - 2015/10

N2 - 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.

AB - 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.

KW - EWI-26665

KW - METIS-315145

KW - IR-98974

U2 - 10.1007/978-3-319-24953-7_1

DO - 10.1007/978-3-319-24953-7_1

M3 - Conference contribution

SN - 978-3-319-24953-7

T3 - Lecture Notes in Computer Science

SP - 1

EP - 3

BT - Automated Technology for Verification and Analysis

PB - Springer

CY - London

ER -

Katoen JP. Probabilistic Programming: A True Verification Challenge. In Finkbeiner B, Pu G, Zhang L, editors, Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings. London: Springer. 2015. p. 1-3. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-24953-7_1