Polar: An Algebraic Analyzer for (Probabilistic) Loops
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910023538442240 |
|---|---|
| author | Moosbrugger, Marcel Müllner, Julian Bartocci, Ezio Kovács, Laura |
| author_facet | Moosbrugger, Marcel Müllner, Julian Bartocci, Ezio Kovács, Laura |
| contents | We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling algebraic recurrences that precisely capture the loop semantics. To this end, our work implements a variety of techniques to compute exact closed-forms of recurrences over higher-order moments of variables, infer invariants, and derive loop sensitivities with respect to unknown parameters. Polar can analyze probabilistic loops containing if-statements, polynomial arithmetic, and common probability distributions. By translating loop analysis into linear recurrence solving, Polar uses the derived closed-forms of recurrences to compute the strongest polynomial invariant or to infer parameter sensitivity. Polar is both sound and complete within well-defined programming model restrictions. Lifting any of these restrictions results in significant hardness limits of computation. To overcome computational burdens for the sake of efficiency, Polar also provides incomplete but sound techniques to compute moments of combinations of variables. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_14573 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Polar: An Algebraic Analyzer for (Probabilistic) Loops Moosbrugger, Marcel Müllner, Julian Bartocci, Ezio Kovács, Laura Programming Languages We present the Polar framework for fully automating the analysis of classical and probabilistic loops using algebraic reasoning. The central theme in Polar comes with handling algebraic recurrences that precisely capture the loop semantics. To this end, our work implements a variety of techniques to compute exact closed-forms of recurrences over higher-order moments of variables, infer invariants, and derive loop sensitivities with respect to unknown parameters. Polar can analyze probabilistic loops containing if-statements, polynomial arithmetic, and common probability distributions. By translating loop analysis into linear recurrence solving, Polar uses the derived closed-forms of recurrences to compute the strongest polynomial invariant or to infer parameter sensitivity. Polar is both sound and complete within well-defined programming model restrictions. Lifting any of these restrictions results in significant hardness limits of computation. To overcome computational burdens for the sake of efficiency, Polar also provides incomplete but sound techniques to compute moments of combinations of variables. |
| title | Polar: An Algebraic Analyzer for (Probabilistic) Loops |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2602.14573 |