A second-order formulation of non-termination
From MaRDI portal
Publication:2353638
DOI10.1016/J.IPL.2015.05.012zbMATH Open1331.68053arXiv1412.3271OpenAlexW1815666329MaRDI QIDQ2353638FDOQ2353638
Authors: Fred Mesnard, Étienne Payet 
Publication date: 15 July 2015
Published in: Information Processing Letters (Search for Journal in Brave)
Abstract: We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient language to express non-termination. Of course, such property is generally undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.
Full work available at URL: https://arxiv.org/abs/1412.3271
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Decidability of theories and sets of sentences (03B25)
Cites Work
- Title not available (Why is that?)
- Decidability of Second-Order Theories and Automata on Infinite Trees
- Monotonicity constraints for termination in the integer domain
- The size-change principle for program termination
- Computer Aided Verification
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Termination of Integer Linear Programs
- Proving non-termination
- On the existence of nonterminating queries for a restricted class of PROLOG-clauses
- Logic Programming
- Deciding conditional termination
Uses Software
This page was built for publication: A second-order formulation of non-termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2353638)
