Mora - Automatic Generation of Moment-Based Invariants

We introduce Mora, an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and...

Descripción completa

Detalles Bibliográficos
Autores principales: Bartocci, Ezio, Kovács, Laura, Stankovič, Miroslav
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439751/
http://dx.doi.org/10.1007/978-3-030-45190-5_28
_version_ 1783573044162199552
author Bartocci, Ezio
Kovács, Laura
Stankovič, Miroslav
author_facet Bartocci, Ezio
Kovács, Laura
Stankovič, Miroslav
author_sort Bartocci, Ezio
collection PubMed
description We introduce Mora, an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, Mora computes invariant properties over higher-order moments of loop variables, expressing, for example, statistical properties, such as expected values and variances, over the value distribution of loop variables.
format Online
Article
Text
id pubmed-7439751
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-74397512020-08-21 Mora - Automatic Generation of Moment-Based Invariants Bartocci, Ezio Kovács, Laura Stankovič, Miroslav Tools and Algorithms for the Construction and Analysis of Systems Article We introduce Mora, an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from symbolic computation and statistics, Mora computes invariant properties over higher-order moments of loop variables, expressing, for example, statistical properties, such as expected values and variances, over the value distribution of loop variables. 2020-03-13 /pmc/articles/PMC7439751/ http://dx.doi.org/10.1007/978-3-030-45190-5_28 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Bartocci, Ezio
Kovács, Laura
Stankovič, Miroslav
Mora - Automatic Generation of Moment-Based Invariants
title Mora - Automatic Generation of Moment-Based Invariants
title_full Mora - Automatic Generation of Moment-Based Invariants
title_fullStr Mora - Automatic Generation of Moment-Based Invariants
title_full_unstemmed Mora - Automatic Generation of Moment-Based Invariants
title_short Mora - Automatic Generation of Moment-Based Invariants
title_sort mora - automatic generation of moment-based invariants
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7439751/
http://dx.doi.org/10.1007/978-3-030-45190-5_28
work_keys_str_mv AT bartocciezio moraautomaticgenerationofmomentbasedinvariants
AT kovacslaura moraautomaticgenerationofmomentbasedinvariants
AT stankovicmiroslav moraautomaticgenerationofmomentbasedinvariants

Ejemplares similares