Proving Termination of Associative Commutative Rewriting Systems by Rewriting. - Isabelle Gnaedig; Pierre Lescanne (CADE, 1986)

Knuth-Bendix procedure and non-deterministic behaviour - An example. - Isabelle Gnaedig (Bull. EATCS, 1987)

Equational Completion in Order-Sorted Algebras (Extended Abstract). - Isabelle Gnaedig; Claude Kirchner; Hélène Kirchner (CAAP, 1988)

Equational Completion in Order-Sorted Algebras. - Isabelle Gnaedig; Claude Kirchner; Hélène Kirchner (Theor. Comput. Sci., 1990)

Termination of Order-sorted Rewriting. - Isabelle Gnaedig (ALP, 1992)

ELIOS-OBJ Theorem Proving in a Specification Language. - Isabelle Gnaedig (ESOP, 1992)

Termination Proofs Using gpo Ordering Constraints. - Thomas Genet; Isabelle Gnaedig (TAPSOFT, 1997)

Termination and normalisation under strategy Proofs in ELAN. - Hélène Kirchner; Isabelle Gnaedig (WRLA, 2000)

Termination of Rewriting with Local Strategies. - Olivier Fissore; Isabelle Gnaedig; Hélène Kirchner (STRATEGIES@IJCAR, 2001)

System Presentation – CARIBOO: An induction based proof tool for termination with strategies. - Olivier Fissore; Isabelle Gnaedig; Hélène Kirchner (PPDP, 2002)

Outermost ground termination. - Olivier Fissore; Isabelle Gnaedig; Hélène Kirchner (WRLA, 2002)

Simplification and termination of strategies in rule-based languages. - Olivier Fissore; Isabelle Gnaedig; Hélène Kirchner (PPDP, 2003)

A Proof of Weak Termination Providing the Right Way to Terminate. - Olivier Fissore; Isabelle Gnaedig; Hélène Kirchner (ICTAC, 2004)

Termination of rewriting strategies: a generic approach - Isabelle Gnaedig; Hélène Kirchner (CoRR, 2005)

Computing constructor forms with non terminating rewrite programs. - Isabelle Gnaedig; Hélène Kirchner (PPDP, 2006)

Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations. - Isabelle Gnaedig; Hélène Kirchner (Rewriting, Computation and Proof, 2007)

Induction for positive almost sure termination. - Isabelle Gnaedig (PPDP, 2007)

Termination of Priority Rewriting. - Isabelle Gnaedig (LATA, 2009)

Termination of rewriting under strategies. - Isabelle Gnaedig; Hélène Kirchner (ACM Trans. Comput. Log., 2009)

Unconditional self-modifying code elimination with dynamic compiler optimizations. - Isabelle Gnaedig; Matthieu Kaczmarek; Daniel Reynaud; Stéphane Wloka (MALWARE, 2010)

Behavior Abstraction in Malware Analysis. - Philippe Beaucamps; Isabelle Gnaedig; Jean-Yves Marion (RV, 2010)

Proving weak properties of rewriting. - Isabelle Gnaedig; Hélène Kirchner (Theor. Comput. Sci., 2011)

Abstraction-Based Malware Analysis Using Rewriting and Model Checking. - Philippe Beaucamps; Isabelle Gnaedig; Jean-Yves Marion (ESORICS, 2012)