Michaël Rusinowitch

Abdessamad Imine, Michaël Rusinowitch: Secure Collaboration for Smartphones. ERCIM News 2013(93) (2013)

Florent Jacquemard, Michaël Rusinowitch: Rewrite Closure and CF Hedge Automata. LATA 2013: 371-382

Walid Belkhir, Yannick Chevalier, Michaël Rusinowitch: Fresh-Variable Automata for Service Composition. CoRR abs/1302.4205 (2013)

Walid Belkhir, Yannick Chevalier, Michaël Rusinowitch: Guarded Variable Automata over Infinite Alphabets. CoRR abs/1304.6297 (2013)

Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch: Unification Modulo Homomorphic Encryption. J. Autom. Reasoning 48(2): 135-158 (2012)

Yannick Chevalier, Michaël Rusinowitch: Decidability of Equivalence of Symbolic Derivations. J. Autom. Reasoning 48(2): 263-292 (2012)

Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch: Unification Modulo Synchronous Distributivity. IJCAR 2012: 14-29

Siva Anantharaman, Christopher Bouchard, Paliath Narendran, Michaël Rusinowitch: Unification Modulo Chaining. LATA 2012: 70-82

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani: Towards the Orchestration of Secured Services under Non-disclosure Policies. MMM-ACNS 2012: 130-145

Alessandro Armando, Wihem Arsac, Tigran Avanesov, Michele Barletta, Alberto Calvi, Alessandro Cappai, Roberto Carbone, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Gabriel Erzse, Simone Frau, Marius Minea, Sebastian Mödersheim, David von Oheimb, Giancarlo Pellegrino, Serena Elisa Ponta, Marco Rocchetto, Michaël Rusinowitch, Mohammad Torabi Dashti, Mathieu Turuani, Luca Viganò: The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. TACAS 2012: 267-282

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani: Intruder deducibility constraints with negation. Decidability and application to secured service compositions. CoRR abs/1207.4871 (2012)

Florent Jacquemard, Michaël Rusinowitch: Rewrite Closure and CF Hedge Automata. CoRR abs/1212.5108 (2012)

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: String Rewriting and Security Analysis: An Extension of a Result of Book and Otto. Journal of Automata, Languages and Combinatorics 16(2-4): 75-90 (2011)

Tigran Avanesov, Yannick Chevalier, Mohammed Anis Mekki, Michaël Rusinowitch: Web Services Verification and Prudent Implementation. DPM/SETOP 2011: 173-189

Tigran Avanesov, Yannick Chevalier, Mohammed Anis Mekki, Michaël Rusinowitch, Mathieu Turuani: Distributed Orchestration of Web Services under Security Constraints. DPM/SETOP 2011: 235-252

Jagdish Prasad Achara, Abdessamad Imine, Michaël Rusinowitch: DeSCal - Decentralized Shared Calendar for P2P and Ad-Hoc Networks. ISPDC 2011: 223-231

Asma Cherif, Abdessamad Imine, Michaël Rusinowitch: Optimistic access control for distributed collaborative editors. SAC 2011: 861-868

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani: Satisfiability of General Intruder Constraints with and without a Set Constructor. CoRR abs/1103.0220 (2011)

Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch: Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator. Fundam. Inform. 105(1-2): 163-187 (2010)

Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch: Efficient decision tree for protocol analysis in intrusion detection. IJSN 5(4): 220-235 (2010)

Yannick Chevalier, Michaël Rusinowitch: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3): 116-122 (2010)

Yannick Chevalier, Michaël Rusinowitch: Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures. Theor. Comput. Sci. 411(10): 1261-1282 (2010)

Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch: Cap unification: application to protocol security modulo homomorphic encryption. ASIACCS 2010: 192-203

Tigran Avanesov, Yannick Chevalier, Michaël Rusinowitch, Mathieu Turuani: Satisfiability of general intruder constraints with a set constructor. CRiSIS 2010: 1-8

Yannick Chevalier, Mohammed Anis Mekki, Michaël Rusinowitch: Orchestration under Security Constraints. FMCO 2010: 23-44

Florent Jacquemard, Michaël Rusinowitch: Rewrite-based verification of XML updates. PPDP 2010: 119-130

Zeeshan Ahmed, Abdessamad Imine, Michaël Rusinowitch: Safe and Efficient Strategies for Updating Firewall Policies. TrustBus 2010: 45-57

Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch: Combinable Extensions of Abelian Groups. CADE 2009: 51-66

Najah Chridi, Mathieu Turuani, Michaël Rusinowitch: Decidable Analysis for a Class of Cryptographic Group Protocols with Unbounded Lists. CSF 2009: 277-289

Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch: Unification Modulo Homomorphic Encryption. FroCoS 2009: 100-116

Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch: Data Structures with Arithmetic Constraints: A Non-disjoint Combination. FroCoS 2009: 319-334

Abdessamad Imine, Asma Cherif, Michaël Rusinowitch: A Flexible Access Control Model for Distributed Collaborative Editors. Secure Data Management 2009: 89-106

Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets. TACAS 2009: 428-442

Florent Jacquemard, Michaël Rusinowitch: Rewrite based Verification of XML Updates. CoRR abs/0907.5125 (2009)

Yannick Chevalier, Michaël Rusinowitch: Compiling and securing cryptographic protocols. CoRR abs/0910.5099 (2009)

Yannick Chevalier, Michaël Rusinowitch: Hierarchical combination of intruder theories. Inf. Comput. 206(2-4): 352-377 (2008)

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron: Tree automata with equality constraints modulo equational theories. J. Log. Algebr. Program. 75(2): 182-208 (2008)

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: Complexity results for security protocols with Diffie-Hellman exponentiation and commuting public key encryption. ACM Trans. Comput. Log. 9(4) (2008)

Humberto J. Abdelnur, Tigran Avanesov, Michaël Rusinowitch, Radu State: Abusing SIP Authentication. IAS 2008: 237-242

Florent Jacquemard, Michaël Rusinowitch: Closure of Hedge-Automata Languages by Hedge Rewriting. RTA 2008: 157-171

Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch: An inference system for detecting firewall filtering rules anomalies. SAC 2008: 2122-2128

Yannick Chevalier, Mohammed Anis Mekki, Michaël Rusinowitch: Automatic Composition of Services with Security Policies. SERVICES I 2008: 529-537

Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu: Relating two standard notions of secrecy. Logical Methods in Computer Science 3(3) (2007)

Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch: A Traffic Classification Algorithm for Intrusion Detection. AINA Workshops (1) 2007: 188-193

Abdessamad Imine, Michaël Rusinowitch: Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms. Rewriting, Computation and Proof 2007: 213-234

Yannick Chevalier, Denis Lugiez, Michaël Rusinowitch: Towards an Automatic Analysis of Web Service Security. FroCoS 2007: 133-147

Yannick Chevalier, Denis Lugiez, Michaël Rusinowitch: Verifying Cryptographic Protocols with Subterms Constraints. LPAR 2007: 181-195

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: Intruders with Caps. RTA 2007: 20-35

Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu: Relating two standard notions of secrecy. CoRR abs/0706.0502 (2007)

Alessandro Armando, David A. Basin, Jorge Cuéllar, Michaël Rusinowitch, Luca Viganò: Automated Reasoning for Security Protocol Analysis. J. Autom. Reasoning 36(1-2): 1-3 (2006)

Abdessamad Imine, Michaël Rusinowitch, Gérald Oster, Pascal Molli: Formal design and verification of operational transformation algorithms for copies convergence. Theor. Comput. Sci. 351(2): 167-183 (2006)

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron: Tree Automata with Equality Constraints Modulo Equational Theories. IJCAR 2006: 557-571

Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu: Relating Two Standard Notions of Secrecy. CSL 2006: 303-318

Eugen Zalinescu, Véronique Cortier, Michaël Rusinowitch: Relating two standard notions of secrecy. Trustworthy Software 2006

Yannick Chevalier, Michaël Rusinowitch: Hierarchical Combination of Intruder Theories. RTA 2006: 108-122

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: Deciding the Security of Protocols with Commuting Public Key Encryption. Electr. Notes Theor. Comput. Sci. 125(1): 55-66 (2005)

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: Closure properties and decision problems of dag automata. Inf. Process. Lett. 94(5): 231-240 (2005)

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: An NP decision procedure for protocol insecurity with XOR. Theor. Comput. Sci. 338(1-3): 247-274 (2005)

Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, Laurent Vigneron: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. CAV 2005: 281-285

Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch: Towards Synchronizing Linear Collaborative Objects with Operational Transformation. FORTE 2005: 411-427

Yannick Chevalier, Michaël Rusinowitch: Combining Intruder Theories. ICALP 2005: 639-651

Véronique Cortier, Michaël Rusinowitch, Eugen Zalinescu: A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures. PPDP 2005: 12-22

Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch: On the fly pattern matching for intrusion detection with Snort. Annales des Télécommunications 59(9-10): 1045-1071 (2004)

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: Unification Modulo ACUI Plus Distributivity Axioms. J. Autom. Reasoning 33(1): 1-28 (2004)

Georg Gottlob, Miki Hermann, Michaël Rusinowitch: 2nd International Workshop on Complexity in Automated Deduction (CiAD) - Foreword. Theory Comput. Syst. 37(6): 639-640 (2004)

Michaël Rusinowitch: Éditorial. Technique et Science Informatiques 23(3): 289-290 (2004)

Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch: Deductive Verification of Distributed Groupware Systems. AMAST 2004: 226-240

Michaël Rusinowitch: A Decidable Analysis of Security Protocols. IFIP TCS 2004: 21

Tarek Abbes, Adel Bouhoula, Michaël Rusinowitch: Protocol Analysis in Intrusion Detection Using Decision Tree. ITCC (1) 2004: 404-408

David A. Basin, Michaël Rusinowitch (Eds.): Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings. Lecture Notes in Computer Science 3097, Springer 2004, isbn 3-540-22345-2

Michaël Rusinowitch: Automated analysis of security protocols. Electr. Notes Theor. Comput. Sci. 86(3): 12-15 (2003)

Alessandro Armando, Silvio Ranise, Michaël Rusinowitch: A rewriting approach to satisfiability procedures. Inf. Comput. 183(2): 140-164 (2003)

Michaël Rusinowitch, Sorin Stratulat, Francis Klay: Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm. J. Autom. Reasoning 30(2): 53-177 (2003)

Michaël Rusinowitch, Mathieu Turuani: Protocol insecurity with a finite number of sessions, composed keys is NP-complete. Theor. Comput. Sci. 1-3(299): 451-475 (2003)

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch: Deciding the confluence of ordered term rewrite systems. ACM Trans. Comput. Log. 4(1): 33-55 (2003)

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: Unification Modulo ACU I Plus Homomorphisms/Distributivity. CADE 2003: 442-457

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani, Laurent Vigneron: Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions. CSL 2003: 128-141

Abdessamad Imine, Pascal Molli, Gérald Oster, Michaël Rusinowitch: Proving Correctness of Transformation Functions Functions in Real-Time Groupware. ECSCW 2003: 277-293

Julien Musset, Michaël Rusinowitch: Computing Meta-transitions for Linear Transition Systems with Polynomials. FME 2003: 562-581

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents. FSTTCS 2003: 124-135

Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, Mathieu Turuani: An NP Decision Procedure for Protocol Insecurity with XOR. LICS 2003: 261-270

Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch: ACID-Unification Is NEXPTIME-Decidable. MFCS 2003: 169-178

Paliath Narendran, Michaël Rusinowitch: Guest Editorial. Inf. Comput. 178(2): 345 (2002)

Alessandro Armando, Michaël Rusinowitch, Sorin Stratulat: Incorporating Decision Procedures in Implicit Induction. J. Symb. Comput. 34(4): 241-258 (2002)

Adel Bouhoula, Michaël Rusinowitch: Observational proofs by rewriting. Theor. Comput. Sci. 275(1-2): 675-698 (2002)

Alessandro Armando, David A. Basin, Mehdi Bouallagui, Yannick Chevalier, Luca Compagna, Sebastian Mödersheim, Michaël Rusinowitch, Mathieu Turuani, Luca Viganò, Laurent Vigneron: The AVISS Security Protocol Analysis Tool. CAV 2002: 349-353

Michaël Rusinowitch: The practice of cryptographic protocol verification. Electr. Notes Theor. Comput. Sci. 55(1): 3-4 (2001)

Rakesh M. Verma, Michaël Rusinowitch, Denis Lugiez: Algorithms and Reductions for Rewriting Problems. Fundam. Inform. 46(3): 257-276 (2001)

Michaël Rusinowitch, Mathieu Turuani: Protocol Insecurity with Finite Number of Sessions is NP-Complete. CSFW 2001: 174-

Alessandro Armando, Silvio Ranise, Michaël Rusinowitch: Uniform Derivation of Decision Procedures by Superposition. CSL 2001: 513-527

Michaël Rusinowitch: Rewriting for Deduction and Verification. RTA 2001: 2

Michaël Rusinowitch, Sorin Stratulat, Francis Klay: Mechanical Verification of an Ideal Incremental ABR Conformance. CAV 2000: 344-357

Paliath Narendran, Michaël Rusinowitch: The Theory of Total Unary RPO Is Decidable. Computational Logic 2000: 660-672

Florent Jacquemard, Michaël Rusinowitch, Laurent Vigneron: Compiling and Verifying Security Protocols. LPAR 2000: 131-160

Gregory Kucherov, Michaël Rusinowitch: Patterns in Words versus Patterns in Trees: A Brief Survey and New Results. Ershov Memorial Conference 1999: 283-296

Paliath Narendran, Michaël Rusinowitch (Eds.): Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings. Lecture Notes in Computer Science 1631, Springer 1999, isbn 3-540-66201-4

Paliath Narendran, Michaël Rusinowitch, Rakesh M. Verma: RPO Constraint Solving Is in NP. CSL 1998: 385-398

Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch: Observational Proofs with Critical Contexts. FASE 1998: 38-53

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch: Decision Problems in Ordered Rewriting. LICS 1998: 276-286

Rakesh M. Verma, Michaël Rusinowitch, Denis Lugiez: Algorithms and Reductions for Rewriting Problems. RTA 1998: 166-180

Gregory Kucherov, Michaël Rusinowitch: Matching a Set of Strings with Variable Length don't Cares. Theor. Comput. Sci. 178(1-2): 129-154 (1997)

Paliath Narendran, Michaël Rusinowitch: Any Ground Associative-Commutative Theory Has a Finite Canonical System. J. Autom. Reasoning 17(1): 131-143 (1996)

Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch: Automated Verification by Induction with Associative-Commutative Operators. CAV 1996: 220-231

Narjes Berregeb, Adel Bouhoula, Michaël Rusinowitch: SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories. RTA 1996: 428-431

Eric Monfroy, Michaël Rusinowitch, René Schott: Implementing non-linear constraints with cooperative solvers. SAC 1996: 63-72

Michaël Rusinowitch, Laurent Vigneron: Automated deduction with associative-commutative operators. Appl. Algebra Eng. Commun. Comput. 6: 23-56 (1995)

Emmanuel Kounalis, Michaël Rusinowitch: Reasoning with Conditional Axioms. Ann. Math. Artif. Intell. 15(2): 125-149 (1995)

Gregory Kucherov, Michaël Rusinowitch: Undecidability of Ground Reducibility for Word Rewriting Systems with Variables. Inf. Process. Lett. 53(4): 209-215 (1995)

Adel Bouhoula, Michaël Rusinowitch: Implicit Induction in Conditional Theories. J. Autom. Reasoning 14(2): 189-235 (1995)

Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch: Automated Mathematical Induction. J. Log. Comput. 5(5): 631-668 (1995)

Adel Bouhoula, Michaël Rusinowitch: SPIKE: A System for Automatic Inductive Proofs. AMAST 1995: 576-577

Gregory Kucherov, Michaël Rusinowitch: Matching a Set of Strings with Variable Length Don't Cares. CPM 1995: 230-247

Gregory Kucherov, Michaël Rusinowitch: The Complexitiy of Testing Ground Reducibility for Linear Word Rewriting Systems with Variables. CTRS 1994: 262-275

Gregory Kucherov, Michaël Rusinowitch: On ground reducibility problem for word rewriting systems with variables. SAC 1994: 271-276

Béchir el Ayeb, Pierre Marquis, Michaël Rusinowitch: Preferring diagnoses by abduction. IEEE Transactions on Systems, Man, and Cybernetics 23(3): 792-808 (1993)

Adel Bouhoula, Michaël Rusinowitch: Automatic Case Analysis in Proof by Induction. IJCAI 1993: 88-94

Paliath Narendran, Michaël Rusinowitch: The Unifiability Problem in Ground AC Theories. LICS 1993: 364-370

Michaël Rusinowitch, Jean-Luc Remy (Eds.): Conditional Term Rewriting Systems, Third International Workshop, CTRS-92, Pont-à-Mousson, France, July 8-10, 1992, Proceedings. Lecture Notes in Computer Science 656, Springer 1993, isbn 3-540-56393-8

Jieh Hsiang, Hélène Kirchner, Pierre Lescanne, Michaël Rusinowitch: The Term Rewriting Approach to Automated Theorem Proving. J. Log. Program. 14(1&2): 71-99 (1992)

Adel Bouhoula, Emmanuel Kounalis, Michaël Rusinowitch: SPIKE, an Automatic Theorem Prover. LPAR 1992: 460-462

Jieh Hsiang, Michaël Rusinowitch: Proving Refutational Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method. J. ACM 38(3): 559-587 (1991)

Michaël Rusinowitch: Theorem-Proving with Resolution and Superposition. J. Symb. Comput. 11(1/2): 21-49 (1991)

Emmanuel Kounalis, Michaël Rusinowitch: On Word Problems in Horn Theories. J. Symb. Comput. 11(1/2): 113-127 (1991)

Emmanuel Kounalis, Michaël Rusinowitch: Studies on the Ground Convergence Property of Conditional Theories. AMAST 1991: 363-376

Michaël Rusinowitch, Laurent Vigneron: Automated deduction with associative commutative operators. FAIR 1991: 185-199

Emmanuel Kounalis, Michaël Rusinowitch: Automatic Proof Methods for Algebraic Specifications. FCT 1991: 307-317

Paliath Narendran, Michaël Rusinowitch: Any Gound Associative-Commutative Theory Has a Finite Canonical System. RTA 1991: 423-434

Emmanuel Kounalis, Michaël Rusinowitch: Mechanizing inductive reasoning. Bulletin of the EATCS 41: 216-226 (1990)

Emmanuel Kounalis, Michaël Rusinowitch: Mechanizing Inductive Reasoning. AAAI 1990: 240-245

Emmanuel Kounalis, Michaël Rusinowitch: A Proof System for Conditional Algebraic Specifications. CTRS 1990: 51-63

Béchir el Ayeb, Pierre Marquis, Michaël Rusinowitch: Deductive/Abductvie Diagnosis: The DA-Principles. ECAI 1990: 47-52

Béchir el Ayeb, Pierre Marquis, Michaël Rusinowitch: A New Diagnosis Approach by Deduction and Abduction. Expert Systems in Engineering 1990: 32-46

Emmanuel Kounalis, Michaël Rusinowitch: On Word Problems in Horn Theories. CADE 1988: 527-537

Michaël Rusinowitch: Theorem-Proving with Resolution and Superposition: An Extension of the Knuth and Bendic Procedure to a Complete Set of Inference Rules. FGCS 1988: 524-531

Michaël Rusinowitch: On Termination of the Direct Sum of Term-Rewriting Systems. Inf. Process. Lett. 26(2): 65-70 (1987)

Michaël Rusinowitch: Path of Subterms Ordering and Recursive Decomposition Ordering Revisited. J. Symb. Comput. 3(1/2): 117-131 (1987)

Emmanuel Kounalis, Michaël Rusinowitch: On Word Problems in Horn Theories. CTRS 1987: 144-160

Jieh Hsiang, Michaël Rusinowitch: On Word Problems in Equational Theories. ICALP 1987: 54-71

Jieh Hsiang, Michaël Rusinowitch, Kô Sakai: Complete Inference Rules for the Cancellation Laws. IJCAI 1987: 990-992

Jieh Hsiang, Michaël Rusinowitch: A New Method for Establishing Refutational Completeness in Theorem Proving. CADE 1986: 141-152

Michaël Rusinowitch: Path of Subterms Ordering and Recursive Decomposition Ordering Revisited. RTA 1985: 225-240