Publications

2024

• Étienne Payet. Non-Termination in Term Rewriting and Logic Programming. Journal of Automated Reasoning, 68(4), 24 pages, Springer, February 2024.

2023

• Étienne Payet. Binary Non-Termination in Term Rewriting and Logic Programming. In Akihisa Yamada, editor, Proc. of the 19th International Workshop on Termination (WST'23). 2023

2022

• Étienne Payet, David J. Pearce and Fausto Spoto. On the Termination of Borrow Checking in Featherweight Rust. In Jyotirmoy V. Deshmukh, Klaus Havelund and Ivan Perez, editors, Proc. of the 14th International NASA Formal Methods Symposium (NFM 2022). Volume 13260 of Lecture Notes in Computer Science, pp. 411-430. Springer Verlag, 2022. Acceptance ratio: 39/118 (33%).

2021

• Étienne Payet. Observing loopingness. In Samir Genaim, editor, Proc. of 17th International Workshop on Termination (WST'21). Pages 69-74, 2021.

2020

• Fred Mesnard, Étienne Payet and Germán Vidal. Selective unification in (constraint) logic programming. Fundamenta Informaticae, 177(3-4):359-383, IOS Press, 2020.
• Fred Mesnard, Étienne Payet and Germán Vidal. Concolic testing in CLP. Theory and Practice of Logic Programming, 20(5):671-686, Cambridge University Press, 2020.
• Sophie Fortz, Fred Mesnard, Étienne Payet, Gilles Perrouin, Wim Vanhoof and Germán Vidal. An SMT-Based Concolic Testing Tool for Logic Programs. In Keisuke Nakano and Konstantinos Sagonas, editors, Proc. of the 15th International Symposium on Functional and Logic Programming (FLOPS 2020). Volume 12073 of Lecture Notes in Computer Science, pp. 215–219. Springer Verlag, 2020.

2018

• Étienne Payet and Fausto Spoto. Checking array bounds by abstract interpretation and symbolic expressions. In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Proc. of the 9th International Joint Conference on Automated Reasoning (IJCAR'18). Volume 10900 of Lecture Notes in Computer Science, pages 706-722. Springer, 2018, ISBN 978-3-319-94204-9. Acceptance ratio: 46/108 (42.6%).
• Étienne Payet. Guided Unfoldings for Finding Loops in Standard Term Rewriting. In Fred Mesnard and Peter Stuckey, editors, Proc. of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'18). Volume 11408 of Lecture Notes in Computer Science, pages 22-37. Springer Verlag, 2019, ISBN 978-3-030-13837-0. Acceptance ratio: 11/29 (37.9%).

2017

• Fred Mesnard, Étienne Payet and Germán Vidal. Selective unification in constraint logic programming. In Wim Vanhoof and Brigitte Pientka, editors, Proc. of the 19th International Symposium on Principles and Practice of Declarative Programming (PPDP'17), pages 115-126. ACM, 2017, ISBN : 978-1-4503-5291-8. Acceptance ratio: 18/28 (64.28%).
• Fonenantsoa Maurica, Fred Mesnard and Étienne Payet. Optimal approximation for efficient termination analysis of floating-point loops. Proc. of the 1st IEEE Conference on Next Generation Computing Applications (NEXTCOMP'17) , 2017.

2016

• Fred Mesnard, Étienne Payet and Germán Vidal. On the completeness of selective unification in concolic testing of logic programs. In Manuel Hermenegildo and Pedro Lopez-Garcia, editors, Proc. of 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'16). Volume 10184 of Lecture Notes in Computer Science, pages 205-221. Springer Verlag, 2017, ISBN 978-3-319-63138-7.
• Fred Mesnard, Étienne Payet and Wim Vanhoof. Towards a framework for algorithm recognition in binary code. In James Cheney and Germán Vidal, editors, Proc. of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP'16), pages 202-213. ACM, 2016, ISBN : 978-1-4503-4148-6. Acceptance ratio: 17/37 (45.94%).
• Fonenantsoa Maurica, Fred Mesnard, and Étienne Payet. Termination analysis of floating-point programs using parameterizable rational approximations. In Sascha Ossowski, editor, Proc. of the 31st ACM/SIGAPP Symposium on Applied Computing (SAC'16), pages 1674-1679. ACM, 2016, ISBN 978-1-4503-3739-7. Acceptance ratio: 252/1047 (24.07%).
• Fonenantsoa Maurica, Fred Mesnard, and Étienne Payet. On the linear ranking problem for simple floating-point loops. In Xavier Rival, editor, Proc. of the 23rd International Static Analysis Symposium (SAS'16). Volume 9837 of Lecture Notes in Computer Science, pages 300-316. Springer Verlag, 2016, ISBN 978-3-662-53412-0. Acceptance ratio: 21/55 (38.18%).

2015

• Fred Mesnard and Étienne Payet. A second-order formulation of non-termination. Information Processing Letters, 115(11):882-885, Elsevier, 2015.
• Fred Mesnard, Étienne Payet and Germán Vidal. Concolic testing in logic programming. Theory and Practice of Logic Programming, 15(4-5):711-725, 2015.

2014

• Étienne Payet and Fausto Spoto. An operational semantics for Android activities. In Wei-Ngan Chin and Jurriaan Hage, editors, Proc. of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM'14), pages 121-132. ACM, 2014, ISBN : 978-1-4503-2619-3.
• Étienne Payet and Fred Mesnard. Non-termination of Dalvik bytecode via compilation to CLP. In Carsten Fuhs, editor, Proc. of 14th International Workshop on Termination (WST'14). Pages 65-69, 2014.

2013

• Étienne Payet. Modeling the Android platform. 8th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'13). Invited speaker. 2013.
• Anthony Alezan, Roberto Bagnara, Fred Mesnard and Étienne Payet. Détection des fonctions de rang linéaires à terme. In Charlotte Truchet, editor, Actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC'13). Pages 11-20, 2013.

2012

• Étienne Payet and Fausto Spoto. Static analysis of Android programs. Information and Software Technology, 54(11):1192-1201, Elsevier, 2012.

2011

• Étienne Payet and Fausto Spoto. Static analysis of Android programs. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, Proc. of the 23rd International Conference on Automated Deduction (CADE'11). Volume 6803 of Lecture Notes in Computer Science, pages 439-445. Springer Verlag, 2011. Acceptance ratio: 35/80 (43.75%).

2010

• Fausto Spoto, Fred Mesnard, and Étienne Payet. A termination analyzer for Java bytecode based on path-length. ACM Transactions on Programming Languages and Systems, 32(3): 70 pages, March 2010.
• Fausto Spoto and Étienne Payet. Magic-sets for localised analysis of Java bytecode. Higher Order and Symbolic Computation, 23(1):29-86, Springer, 2010.

2009

• Étienne Payet and Fred Mesnard. A non-termination criterion for binary constraint logic programs. Theory and Practice of Logic Programming, 9(2):145-164, 2009.
• Étienne Payet and Fausto Spoto. Experiments with non-termination analysis for Java bytecode. In Elvira Albert and Samir Genaim, editors, Proc. of the 4th International Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'09). Volume 253 of Electronic Notes in Theoretical Computer Science, Issue 5, pages 83-96. 2009. Long version with formal definitions, theorems and proofs.

2008

• Étienne Payet. Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science, 403(2-3):307-327, Elsevier, 2008.

2007

• Étienne Payet and Fausto Spoto. Magic-sets transformation for the analysis of Java bytecode. In Gilberto Filé and Hanne Riis Nielson, editors, Proc. of the 14th International Static Analysis Symposium (SAS'07). Volume 4634 of Lecture Notes in Computer Science, pages 452-467. Springer Verlag, 2007. Acceptance ratio: 26/85 (30.59%).

2006

• Étienne Payet. Detecting non-termination of term rewriting systems using an unfolding operator. In Germán Puebla, editor, Proc. of the 16th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR'06). Volume 4407 of Lecture Notes in Computer Science, pages 194-209. Springer Verlag, 2006.
• Étienne Payet and Fred Mesnard. Non-termination inference of logic programs. ACM Transactions on Programming Languages and Systems, 28(2):256-289, March 2006.
• Fausto Spoto, Patricia M. Hill, and Étienne Payet. Path-length analysis for object-oriented programs. Presented at the First International Workshop on Emerging Applications of Abstract Interpretation (EAAI'06). 2006.

2005

• Étienne Payet and Fred Mesnard. An improved non-termination criterion for binary constraint logic programs. In Susana Muñoz-Hernández and Alexander Serebrenik, editors, Proc. of the 15th International Workshop on Logic Programming Environments (WLPE'05). Pages 46-60, 2005.

2004

• Étienne Payet and Fred Mesnard. Non-termination inference for constraint logic programs. In Roberto Giacobazzi, editor, Proc. of the 11th International Static Analysis Symposium (SAS'04). Volume 3148 of Lecture Notes in Computer Science, pages 377-392. Springer Verlag, 2004. Acceptance ratio: 23/63 (36.51%).
• Étienne Payet and Fred Mesnard. Inférence de non-terminaison pour les programmes logiques avec contraintes. In Fred Mesnard, editor, Actes des 13èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC'04). Pages 55-72. Hermès, 2004.

2002

• Fred Mesnard, Étienne Payet, and Ulrich Neumerkel. Detecting optimal termination conditions of logic programs. In Manuel Hermenegildo and Germán Puebla, editors, Proc. of the 9th International Static Analysis Symposium (SAS'02). Volume 2477 of Lecture Notes in Computer Science, pages 509-525. Springer Verlag, 2002. Acceptance ratio: 32/86 (37.21%).
• Fred Mesnard, Étienne Payet, and Ulrich Neumerkel. Non-termination inference and optimal termination conditions of logic programs. Actes des 11èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC'02). Pages 87-104. Hermès, 2002.

2001

• Fred Mesnard, Ulrich Neumerkel, and Étienne Payet. cTI: un outil pour l'inférence de conditions optimales de terminaison pour Prolog. Actes des 10èmes Journées Francophones de Programmation en Logique et Programmation par Contraintes (JFPLC'01). Pages 271-286. Hermès, 2001.

2000

• Étienne Payet. Thue specifications, infinite graphs and synchronized product. Fundamenta Informaticae, 44(3):265-290, IOS Press, 2000.
• Étienne Payet. Produit synchronisé pour quelques classes de graphes infinis (Synchronized product for some classes of infinite graphs). PhD, university of Reunion, 2000.

1999

• Teodor Knapik and Étienne Payet. Synchronized product of linear bounded machines. In Gabriel Ciobanu and Gheorghe Pãun, editors, Proc. of the 12th International Symposium on Fundamentals of Computation Theory (FCT'99). Volume 1684 of Lecture Notes in Computer Science, pages 362-373. Springer Verlag, 1999. Acceptance ratio: 42/104 (40.38%).

1998

• Teodor Knapik and Étienne Payet. The full quotient and its closure property for regular languages. Information Processing Letters, 65(2):57-62, Elsevier, 1998.