Prinsys - On a quest for probabilistic loop invariants

Friedrich Gretz, Joost Pieter Katoen, Annabelle McIver

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

12 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems
Subtitle of host publication10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings
EditorsKaustubh Joshi, Markus Siegle, Mariëlle Stoelinga, Pedro R. D’Argenio
Place of PublicationHeidelberg
PublisherSpringer, Springer Nature
Pages193-208
Number of pages16
ISBN (Electronic)9783642401961
ISBN (Print)9783642401954
DOIs
Publication statusPublished - 2013
Event10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013

Publication series

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

Other

Other10th International Conference on Quantitative Evaluation of Systems, QEST 2013
CountryArgentina
CityBuenos Aires
Period27/08/1330/08/13

Keywords

  • invariant generation
  • probabilistic programs
  • non-linear constraint solving

Fingerprint Dive into the research topics of 'Prinsys - On a quest for probabilistic loop invariants'. Together they form a unique fingerprint.

  • Cite this

    Gretz, F., Katoen, J. P., & McIver, A. (2013). Prinsys - On a quest for probabilistic loop invariants. In K. Joshi, M. Siegle, M. Stoelinga, & P. R. D’Argenio (Eds.), Quantitative Evaluation of Systems: 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings (pp. 193-208). (Lecture Notes in Computer Science; Vol. 8054). Heidelberg: Springer, Springer Nature. https://doi.org/10.1007/978-3-642-40196-1_17