A second-order formulation of non-termination

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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01451689
Contributor : Réunion Univ <>
Submitted on : Monday, November 5, 2018 - 11:09:18 AM
Last modification on : Thursday, March 28, 2019 - 11:24:10 AM
Long-term archiving on : Wednesday, February 6, 2019 - 2:33:23 PM

File

1412.3271.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Frédéric Mesnard, Etienne Payet. A second-order formulation of non-termination. Information Processing Letters, Elsevier, 2015, 115 (11), pp.882--885. ⟨10.1016/j.ipl.2015.05.012⟩. ⟨hal-01451689⟩

Share

Metrics

Record views

46

Files downloads

64