A second-order formulation of non-termination

DOI10.1016/J.IPL.2015.05.012MaRDI QIDQ2353638zbMATH OpenOpenAlexFDO

Authors Fred Mesnard, Étienne Payet

Publication date 15 July 2015

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1412.3271

zbMATH Keywords

monadic second-order logicprogram correctnessterminationnon-termination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Decidability of theories and sets of sentences (03B25)

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.

Recommendations

• Non-termination Sets of Simple Linear Loops
• Deciding conditional termination
• Deciding conditional termination
• Termination analysis of nonlinear loops over closed and bounded connected domain
• Termination of polynomial loops

Cites work

• scientific article; zbMATH DE number 1142314 (Why is no real title available?)
• scientific article; zbMATH DE number 3237829 (Why is no real title available?)
• Computer Aided Verification
• Decidability of Second-Order Theories and Automata on Infinite Trees
• Deciding conditional termination
• Logic Programming
• Monotonicity constraints for termination in the integer domain
• On the existence of nonterminating queries for a restricted class of PROLOG-clauses
• Proving non-termination
• Termination of Integer Linear Programs
• The size-change principle for program termination
• Verification, Model Checking, and Abstract Interpretation

Describes a project that uses

Uses Software

• MONA

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)