---
_id: '9644'
abstract:
- lang: eng
  text: 'We present a new approach to proving non-termination of non-deterministic
    integer programs. Our technique is rather simple but efficient. It relies on a
    purely syntactic reversal of the program''s transition system followed by a constraint-based
    invariant synthesis with constraints coming from both the original and the reversed
    transition system. The latter task is performed by a simple call to an off-the-shelf
    SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover,
    our method offers a combination of features not present (as a whole) in previous
    approaches: it handles programs with non-determinism, provides relative completeness
    guarantees and supports programs with polynomial arithmetic. The experiments performed
    with our prototype tool RevTerm show that our approach, despite its simplicity
    and stronger theoretical guarantees, is at least on par with the state-of-the-art
    tools, often achieving a non-trivial improvement under a proper configuration
    of its parameters.'
acknowledgement: We thank the anonymous reviewers for their helpful comments. This
  research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech
  Science Foundation grant No. GJ19-15134Y.
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ehsan Kafshdar
  full_name: Goharshady, Ehsan Kafshdar
  last_name: Goharshady
- first_name: Petr
  full_name: Novotný, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotný
- first_name: Dorde
  full_name: Zikelic, Dorde
  id: 294AA7A6-F248-11E8-B48F-1D18A9856A87
  last_name: Zikelic
  orcid: 0000-0002-4681-1699
citation:
  ama: 'Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination
    by program reversal. In: <i>Proceedings of the 42nd ACM SIGPLAN International
    Conference on Programming Language Design and Implementation</i>. Association
    for Computing Machinery; 2021:1033-1048. doi:<a href="https://doi.org/10.1145/3453483.3454093">10.1145/3453483.3454093</a>'
  apa: 'Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021).
    Proving non-termination by program reversal. In <i>Proceedings of the 42nd ACM
    SIGPLAN International Conference on Programming Language Design and Implementation</i>
    (pp. 1033–1048). Online: Association for Computing Machinery. <a href="https://doi.org/10.1145/3453483.3454093">https://doi.org/10.1145/3453483.3454093</a>'
  chicago: Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde
    Zikelic. “Proving Non-Termination by Program Reversal.” In <i>Proceedings of the
    42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>,
    1033–48. Association for Computing Machinery, 2021. <a href="https://doi.org/10.1145/3453483.3454093">https://doi.org/10.1145/3453483.3454093</a>.
  ieee: K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination
    by program reversal,” in <i>Proceedings of the 42nd ACM SIGPLAN International
    Conference on Programming Language Design and Implementation</i>, Online, 2021,
    pp. 1033–1048.
  ista: 'Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination
    by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference
    on Programming Language Design and Implementation. PLDI: Programming Language
    Design and Implementation, 1033–1048.'
  mla: Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.”
    <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
    Language Design and Implementation</i>, Association for Computing Machinery, 2021,
    pp. 1033–48, doi:<a href="https://doi.org/10.1145/3453483.3454093">10.1145/3453483.3454093</a>.
  short: K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048.
conference:
  end_date: 2021-06-26
  location: Online
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2021-06-20
date_created: 2021-07-11T22:01:17Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2025-07-14T09:10:06Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3453483.3454093
ec_funded: 1
external_id:
  arxiv:
  - '2104.01189'
  isi:
  - '000723661700067'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2104.01189
month: '06'
oa: 1
oa_version: Preprint
page: 1033-1048
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
  Language Design and Implementation
publication_identifier:
  isbn:
  - '9781450383912'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '14539'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Proving non-termination by program reversal
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '9645'
abstract:
- lang: eng
  text: "We consider the fundamental problem of reachability analysis over imperative
    programs with real variables. Previous works that tackle reachability are either
    unable to handle programs consisting of general loops (e.g. symbolic execution),
    or lack completeness guarantees (e.g. abstract interpretation), or are not automated
    (e.g. incorrectness logic). In contrast, we propose a novel approach for reachability
    analysis that can handle general and complex loops, is complete, and can be entirely
    automated for a wide family of programs. Through the notion of Inductive Reachability
    Witnesses (IRWs), our approach extends ideas from both invariant generation and
    termination to reachability analysis.\r\n\r\nWe first show that our IRW-based
    approach is sound and complete for reachability analysis of imperative programs.
    Then, we focus on linear and polynomial programs and develop automated methods
    for synthesizing linear and polynomial IRWs. In the linear case, we follow the
    well-known approaches using Farkas' Lemma. Our main contribution is in the polynomial
    case, where we present a push-button semi-complete algorithm. We achieve this
    using a novel combination of classical theorems in real algebraic geometry, such
    as Putinar's Positivstellensatz and Hilbert's Strong Nullstellensatz. Finally,
    our experimental results show we can prove complex reachability objectives over
    various benchmarks that were beyond the reach of previous methods."
acknowledgement: This research was partially supported by the ERC CoG 863818 (ForM-SMArt),
  the National Natural Science Foundation of China (NSFC) Grant No. 61802254, the
  Huawei Innovation Research Program, the Facebook PhD Fellowship Program, and DOC
  Fellowship No. 24956 of the Austrian Academy of Sciences (ÖAW).
article_processing_charge: No
author:
- first_name: Ali
  full_name: Asadi, Ali
  last_name: Asadi
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Mohammad
  full_name: Mahdavi, Mohammad
  last_name: Mahdavi
citation:
  ama: 'Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. Polynomial reachability
    witnesses via Stellensätze. In: <i>Proceedings of the 42nd ACM SIGPLAN International
    Conference on Programming Language Design and Implementation</i>. Association
    for Computing Machinery; 2021:772-787. doi:<a href="https://doi.org/10.1145/3453483.3454076">10.1145/3453483.3454076</a>'
  apa: 'Asadi, A., Chatterjee, K., Fu, H., Goharshady, A. K., &#38; Mahdavi, M. (2021).
    Polynomial reachability witnesses via Stellensätze. In <i>Proceedings of the 42nd
    ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>
    (pp. 772–787). Online: Association for Computing Machinery. <a href="https://doi.org/10.1145/3453483.3454076">https://doi.org/10.1145/3453483.3454076</a>'
  chicago: Asadi, Ali, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady,
    and Mohammad Mahdavi. “Polynomial Reachability Witnesses via Stellensätze.” In
    <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
    Language Design and Implementation</i>, 772–87. Association for Computing Machinery,
    2021. <a href="https://doi.org/10.1145/3453483.3454076">https://doi.org/10.1145/3453483.3454076</a>.
  ieee: A. Asadi, K. Chatterjee, H. Fu, A. K. Goharshady, and M. Mahdavi, “Polynomial
    reachability witnesses via Stellensätze,” in <i>Proceedings of the 42nd ACM SIGPLAN
    International Conference on Programming Language Design and Implementation</i>,
    Online, 2021, pp. 772–787.
  ista: 'Asadi A, Chatterjee K, Fu H, Goharshady AK, Mahdavi M. 2021. Polynomial reachability
    witnesses via Stellensätze. Proceedings of the 42nd ACM SIGPLAN International
    Conference on Programming Language Design and Implementation.  PLDI: Programming
    Language Design and Implementation, 772–787.'
  mla: Asadi, Ali, et al. “Polynomial Reachability Witnesses via Stellensätze.” <i>Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation</i>, Association for Computing Machinery, 2021, pp. 772–87,
    doi:<a href="https://doi.org/10.1145/3453483.3454076">10.1145/3453483.3454076</a>.
  short: A. Asadi, K. Chatterjee, H. Fu, A.K. Goharshady, M. Mahdavi, in:, Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation, Association for Computing Machinery, 2021, pp. 772–787.
conference:
  end_date: 2021-06-26
  location: Online
  name: ' PLDI: Programming Language Design and Implementation'
  start_date: 2021-06-20
date_created: 2021-07-11T22:01:17Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2025-07-14T09:10:06Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3453483.3454076
ec_funded: 1
external_id:
  isi:
  - '000723661700050'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://hal.archives-ouvertes.fr/hal-03183862/
month: '06'
oa: 1
oa_version: Submitted Version
page: 772-787
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 267066CE-B435-11E9-9278-68D0E5697425
  name: Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
  Language Design and Implementation
publication_identifier:
  isbn:
  - '9781450383912'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Polynomial reachability witnesses via Stellensätze
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '9646'
abstract:
- lang: eng
  text: We consider the fundamental problem of deriving quantitative bounds on the
    probability that a given assertion is violated in a probabilistic program. We
    provide automated algorithms that obtain both lower and upper bounds on the assertion
    violation probability. The main novelty of our approach is that we prove new and
    dedicated fixed-point theorems which serve as the theoretical basis of our algorithms
    and enable us to reason about assertion violation bounds in terms of pre and post
    fixed-point functions. To synthesize such fixed-points, we devise algorithms that
    utilize a wide range of mathematical tools, including repulsing ranking supermartingales,
    Hoeffding's lemma, Minkowski decompositions, Jensen's inequality, and convex optimization.
    On the theoretical side, we provide (i) the first automated algorithm for lower-bounds
    on assertion violation probabilities, (ii) the first complete algorithm for upper-bounds
    of exponential form in affine programs, and (iii) provably and significantly tighter
    upper-bounds than the previous approaches. On the practical side, we show our
    algorithms can handle a wide variety of programs from the literature and synthesize
    bounds that are remarkably tighter than previous results, in some cases by thousands
    of orders of magnitude.
acknowledgement: 'We are very thankful to the anonymous reviewers for the helpful
  and valuable comments. The work was partially supported by the National Natural
  Science Foundation of China (NSFC) Grant No. 61802254, the Huawei Innovation Research
  Program, the ERC CoG 863818 (ForM-SMArt), the Facebook PhD Fellowship Program and
  DOC Fellowship #24956 of the Austrian Academy of Sciences (ÖAW).'
article_processing_charge: No
arxiv: 1
author:
- first_name: Jinyi
  full_name: Wang, Jinyi
  last_name: Wang
- first_name: Yican
  full_name: Sun, Yican
  last_name: Sun
- first_name: Hongfei
  full_name: Fu, Hongfei
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Amir Kafshdar
  full_name: Goharshady, Amir Kafshdar
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
citation:
  ama: 'Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. Quantitative analysis of
    assertion violations in probabilistic programs. In: <i>Proceedings of the 42nd
    ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>.
    Association for Computing Machinery; 2021:1171-1186. doi:<a href="https://doi.org/10.1145/3453483.3454102">10.1145/3453483.3454102</a>'
  apa: 'Wang, J., Sun, Y., Fu, H., Chatterjee, K., &#38; Goharshady, A. K. (2021).
    Quantitative analysis of assertion violations in probabilistic programs. In <i>Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation</i> (pp. 1171–1186). Online: Association for Computing Machinery.
    <a href="https://doi.org/10.1145/3453483.3454102">https://doi.org/10.1145/3453483.3454102</a>'
  chicago: Wang, Jinyi, Yican Sun, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar
    Goharshady. “Quantitative Analysis of Assertion Violations in Probabilistic Programs.”
    In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
    Language Design and Implementation</i>, 1171–86. Association for Computing Machinery,
    2021. <a href="https://doi.org/10.1145/3453483.3454102">https://doi.org/10.1145/3453483.3454102</a>.
  ieee: J. Wang, Y. Sun, H. Fu, K. Chatterjee, and A. K. Goharshady, “Quantitative
    analysis of assertion violations in probabilistic programs,” in <i>Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation</i>, Online, 2021, pp. 1171–1186.
  ista: 'Wang J, Sun Y, Fu H, Chatterjee K, Goharshady AK. 2021. Quantitative analysis
    of assertion violations in probabilistic programs. Proceedings of the 42nd ACM
    SIGPLAN International Conference on Programming Language Design and Implementation.
    PLDI: Programming Language Design and Implementation, 1171–1186.'
  mla: Wang, Jinyi, et al. “Quantitative Analysis of Assertion Violations in Probabilistic
    Programs.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on
    Programming Language Design and Implementation</i>, Association for Computing
    Machinery, 2021, pp. 1171–86, doi:<a href="https://doi.org/10.1145/3453483.3454102">10.1145/3453483.3454102</a>.
  short: J. Wang, Y. Sun, H. Fu, K. Chatterjee, A.K. Goharshady, in:, Proceedings
    of the 42nd ACM SIGPLAN International Conference on Programming Language Design
    and Implementation, Association for Computing Machinery, 2021, pp. 1171–1186.
conference:
  end_date: 2021-06-26
  location: Online
  name: 'PLDI: Programming Language Design and Implementation'
  start_date: 2021-06-20
date_created: 2021-07-11T22:01:18Z
date_published: 2021-06-01T00:00:00Z
date_updated: 2025-07-14T09:10:06Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3453483.3454102
ec_funded: 1
external_id:
  arxiv:
  - '2011.14617'
  isi:
  - '000723661700076'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/2011.14617
month: '06'
oa: 1
oa_version: Preprint
page: 1171-1186
project:
- _id: 0599E47C-7A3F-11EA-A408-12923DDC885E
  call_identifier: H2020
  grant_number: '863818'
  name: 'Formal Methods for Stochastic Models: Algorithms and Applications'
- _id: 267066CE-B435-11E9-9278-68D0E5697425
  name: Quantitative Analysis of Probablistic Systems with a focus on Crypto-currencies
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
  Language Design and Implementation
publication_identifier:
  isbn:
  - '9781450383912'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Quantitative analysis of assertion violations in probabilistic programs
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...