---
res:
  bibo_abstract:
  - "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.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Ali
      foaf_name: Asadi, Ali
      foaf_surname: Asadi
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Hongfei
      foaf_name: Fu, Hongfei
      foaf_surname: Fu
      foaf_workInfoHomepage: http://www.librecat.org/personId=3AAD03D6-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Amir Kafshdar
      foaf_name: Goharshady, Amir Kafshdar
      foaf_surname: Goharshady
      foaf_workInfoHomepage: http://www.librecat.org/personId=391365CE-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0003-1702-6584
  - foaf_Person:
      foaf_givenName: Mohammad
      foaf_name: Mahdavi, Mohammad
      foaf_surname: Mahdavi
  bibo_doi: 10.1145/3453483.3454076
  dct_date: 2021^xs_gYear
  dct_identifier:
  - UT:000723661700050
  dct_isPartOf:
  - http://id.crossref.org/issn/9781450383912
  dct_language: eng
  dct_publisher: Association for Computing Machinery@
  dct_title: Polynomial reachability witnesses via Stellensätze@
...