• DocumentCode
    2215827
  • Title

    Termination of programs over the union of intervals

  • Author

    Mu, Lin ; Li, Yi ; Jin, Taige ; Luo, Jiawei

  • Author_Institution
    Lab. for Automated Reasoning & Programming, CAS, Chengdu, China
  • Volume
    1
  • fYear
    2010
  • fDate
    20-22 Aug. 2010
  • Abstract
    For a generic loop: while (constraints) {updates} it is well known that the termination problem is undecidable in general, even for a simple class of polynomial programs. If the constraints or the updating function in the above loop is not linear, the loop is called nonlinear. In this paper, we investigate how to solve the termination of the above loop by deciding whether a fixed point exists, when the constraints are the union of intervals and the updating functions are polynomials. Furthermore, when all fixed points are on the boundaries of the union of intervals, we also establish a corresponding necessary and sufficient condition of nontermination.
  • Keywords
    constraint handling; nonlinear programming; polynomials; program control structures; program verification; generic loop; nonlinear loop; polynomial program; program termination; union of intervals; updating function; Orbits; Fixed point; Nonlinear Program; Program Verification; Termination Analysis;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Advanced Computer Theory and Engineering (ICACTE), 2010 3rd International Conference on
  • Conference_Location
    Chengdu
  • ISSN
    2154-7491
  • Print_ISBN
    978-1-4244-6539-2
  • Type

    conf

  • DOI
    10.1109/ICACTE.2010.5579031
  • Filename
    5579031