Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

O-minimal invariants for linear loops

Tools
- Tools
+ Tools

Almagor, Shaull, Chistikov, Dmitry, Ouaknine, Joel and Worrell, James (2018) O-minimal invariants for linear loops. In: ICALP 2018: 45th International Colloquium on Automata, Languages, and Programming, Prague, Czech Republic, 9-13 Jul 2018. Published in: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), 107 114:1-114:14. ISBN 9783959770767. ISSN 1868-8969. doi:10.4230/LIPIcs.ICALP.2018.114

[img]
Preview
PDF
WRAP-O-minimal-invariants-for-linear-loops-Chistikov-2018.pdf - Published Version - Requires a PDF viewer.
Available under License Creative Commons Attribution.

Download (577Kb) | Preview
Official URL: http://doi.org/10.4230/LIPIcs.ICALP.2018.114

Request Changes to record.

Abstract

The termination analysis of linear loops plays a key role in several areas of computer science, including program verification and abstract interpretation. Such deceptively simple questions also relate to a number of deep open problems, such as the decidability of the Skolem and Positivity Problems for linear recurrence sequences, or equivalently reachability questions for discrete-time linear dynamical systems. In this paper, we introduce the class of \emph{o-minimal invariants}, which is broader than any previously considered, and study the decidability of the existence and algorithmic synthesis of such invariants as certificates of non-termination for linear loops equipped with a large class of halting conditions. We establish two main decidability results, one of them conditional on Schanuel's conjecture.

Item Type: Conference Item (Paper)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science > Computer Science
Library of Congress Subject Headings (LCSH): Invariants, Dynamics, Algorithms
Series Name: Leibniz International Proceedings in Informatics (LIPIcs)
Journal or Publication Title: 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)
Publisher: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Place of Publication: Germany
ISBN: 9783959770767
ISSN: 1868-8969
Official Date: 2018
Dates:
DateEvent
2018Published
16 April 2018Accepted
Date of first compliant deposit: 4 May 2018
Volume: 107
Page Range: 114:1-114:14
DOI: 10.4230/LIPIcs.ICALP.2018.114
Status: Peer Reviewed
Publication Status: Published
Access rights to Published version: Open Access
RIOXX Funder/Project Grant:
Project/Grant IDRIOXX Funder NameFunder ID
EP/N008197/1[EPSRC] Engineering and Physical Sciences Research Councilhttp://dx.doi.org/10.13039/501100000266
UNSPECIFIEDEuropean Research Councilhttp://viaf.org/viaf/130022607
Conference Paper Type: Paper
Title of Event: ICALP 2018: 45th International Colloquium on Automata, Languages, and Programming
Type of Event: Conference
Location of Event: Prague, Czech Republic
Date(s) of Event: 9-13 Jul 2018
Related URLs:
  • Organisation
  • Other Repository
  • Publisher
Open Access Version:
  • ArXiv

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us