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.
Type de document :
Article dans une revue
Information Processing Letters, Elsevier, 2015, 115 (11), pp.882--885. 〈10.1016/j.ipl.2015.05.012〉
Liste complète des métadonnées

http://hal.univ-reunion.fr/hal-01451689
Contributeur : Réunion Univ <>
Soumis le : lundi 5 novembre 2018 - 11:09:18
Dernière modification le : mercredi 7 novembre 2018 - 06:37:48

Fichier

1412.3271.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

17

Téléchargements de fichiers

5