VLDB 2026 Research / reviewers in the wild / expert
Jiri Zárevúcky
dblp:272/9265
· DBLP profile ↗
2ranked-venue papers
0as first author
2since 2021 · last 2023
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 2 · 2 since 2021Software engineering, systems software and programming languages · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2023 | On Lexicographic Proof Rules for Probabilistic TerminationabstractWe consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný 0001, Jiri Zárevúcky, Dorde Zikelic |
Formal Aspects Comput. | 4 |
| 2021 | On Lexicographic Proof Rules for Probabilistic Termination
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný 0001, Jiri Zárevúcky, Dorde Zikelic |
FM | 4 |