Prinsys - On a quest for probabilistic loop invariants

Friedrich Gretz, Joost Pieter Katoen, Annabelle McIver

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

13 Citations (Scopus)


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
Number of pages16
ISBN (Electronic)9783642401961
ISBN (Print)9783642401954
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
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other10th International Conference on Quantitative Evaluation of Systems, QEST 2013
CityBuenos Aires


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


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

Cite this