@inproceedings{3fd0867ec59043478c757383dfd3fc42,
title = "Prinsys - On a quest for probabilistic loop invariants",
abstract = "Prinsys (pronounced {"}princess{"}) is a new software-tool for probabilistic invariant synthesis. In this paper we discuss its implementation and improvements of the methodology which was set out in previous work. In particular we have substantially simplified the method and generalised it to non-linear programs and invariants. Prinsys follows a constraint-based approach. A given parameterised loop annotation is speculatively placed in the program. The tool returns a formula that captures precisely the invariant instances of the given candidate. Our approach is sound and complete. Prinsys's applicability is evaluated on several examples. We believe the tool contributes to the successful analysis of sequential probabilistic programs with infinite-domain variables and parameters.",
keywords = "invariant generation, probabilistic programs, non-linear constraint solving",
author = "Friedrich Gretz and Katoen, {Joost Pieter} and Annabelle McIver",
year = "2013",
doi = "10.1007/978-3-642-40196-1_17",
language = "English",
isbn = "9783642401954",
series = "Lecture Notes in Computer Science",
publisher = "Springer, Springer Nature",
pages = "193--208",
editor = "Kaustubh Joshi and Markus Siegle and Mari{\"e}lle Stoelinga and D’Argenio, {Pedro R.}",
booktitle = "Quantitative Evaluation of Systems",
address = "United States",
}