Christopher Lynch

Stephen Miner

Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023) co-located with the 29th International Conference on Automated Deduction (CADE 2023), 2023

2022

CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms.

[BibT_eX]

[DOI]

Proceedings of the 13th International Symposium on Games, 2022

2021

Congruence Closure Modulo Permutation Equations.

[BibT_eX]

[DOI]

Proceedings of the 9th International Symposium on Symbolic Computation in Software Science, 2021

An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Formal Analysis of Symbolic Authenticity.

[BibT_eX]

[DOI]

Hai Lin

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Equational Theorem Proving Modulo.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Bounded ACh unification.

[BibT_eX]

[DOI]

Ajay Kumar Eeralla

Math. Struct. Comput. Sci., 2020

Local XOR Unification: Definitions, Algorithms and Application to Cryptography.

[BibT_eX]

[DOI]

Hai Lin

IACR Cryptol. ePrint Arch., 2020

2019

On Asymmetric Unification for the Theory of XOR with a Homomorphism.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

Reviving Basic Narrowing Modulo.

[BibT_eX]

[DOI]

Paliath Narendran

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

Finding Intruder Knowledge with Cap-Matching.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Security, Protocols, and Equational Reasoning, 2019

2014

Efficient general AGH-unification.

[BibT_eX]

[DOI]

Zhiqiang Liu

Inf. Comput., 2014

2013

SMELS: Satisfiability Modulo Equality with Lazy Superposition.

[BibT_eX]

[DOI]

Quang-Trung Ta

J. Autom. Reason., 2013

On Forward Closure and the Finite Variant Property.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-24, 2013

Constructing Bachmair-Ganzinger Models.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

Unification Modulo Homomorphic Encryption.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions.

[BibT_eX]

[DOI]

Proceedings of the Computer Security - ESORICS 2012, 2012

Unification Modulo Synchronous Distributivity.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

On Deciding Satisfiability by Theorem Proving with Speculative Inferences.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Leonardo Mendonça de Moura

J. Autom. Reason., 2011

Automatic decidability and combinability.

[BibT_eX]

[DOI]

Silvio Ranise

Christophe Ringeissen

Inf. Comput., 2011

Invited talk: Unification in Cryptographic Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the 25th International Workshop on Unification, 2011

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis.

[BibT_eX]

[DOI]

Proceedings of the 25th International Workshop on Unification, 2011

Unification in a Theory of Blind Signatures.

[BibT_eX]

Serdar Erbatur

Paliath Narendran

Proceedings of the TABLEAUX 2011, 2011

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption.

[BibT_eX]

[DOI]

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Efficient General Unification for XOR with Homomorphism.

[BibT_eX]

[DOI]

Zhiqiang Liu

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Preface.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Frontmatter (Titlepage, Table of Contents, Author List, PC List, Reviewer List).

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Rewriting Techniques and Applications, 2010

Cap unification: application to protocol security modulo homomorphic encryption.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM Symposium on Information, 2010

2009

Combining Instance Generation and Resolution.

[BibT_eX]

[DOI]

Ralph Eric McGregor

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

On Deciding Satisfiability by DPLL(G+<i>T</i>) and Unsound Theorem Proving.

[BibT_eX]

[DOI]

Maria Paola Bonacina

Leonardo Mendonça de Moura

Proceedings of the Automated Deduction, 2009

2008

Rewriting Interpolants.

[BibT_eX]

[DOI]

Yuefeng Tang

Proceedings of the First International Conference on Foundations of Informatics, 2008

Unification modulo Homomorphic Encryption is Decidable.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Workshop on Unification, 2008

SMELS: Satisfiability Modulo Equality with Lazy Superposition.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

Interpolants for Linear Arithmetic in SMT.

[BibT_eX]

[DOI]

Yuefeng Tang

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

Encoding First Order Proofs in SMT.

[BibT_eX]

[DOI]

Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Protocol Verification Via Rigid/Flexible Resolution.

[BibT_eX]

[DOI]

Stéphanie Delaune

Hai Lin

Proceedings of the Logic for Programming, 2007

Parallel Type-2 Fuzzy Logic Co-Processors for Engine Management.

[BibT_eX]

[DOI]

Hani Hagras

Victor Callaghan

Proceedings of the FUZZ-IEEE 2007, 2007

Automatic Decidability and Combinability Revisited.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

Encoding First Order Proofs in SAT.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2007

2006

Using Uncertainty Bounds in the Design of an Embedded Real-Time Type-2 Neuro-Fuzzy Speed Controller for Marine Diesel Engines.

[BibT_eX]

[DOI]

Hani Hagras

Victor Callaghan

Proceedings of the IEEE International Conference on Fuzzy Systems, 2006

2005

Faster <i>Basic Syntactic Mutation</i> with Sorts for Some Separable Equational Theories.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Embedded Type-2 FLC for Real-Time Speed Control of Marine and Traction Diesel Engines.

[BibT_eX]

[DOI]

Hani Hagras

Victor Callaghan

Proceedings of the IEEE International Conference on Fuzzy Systems, 2005

2004

On the Relative Soundness of the Free Algebra Model for Public Key Encryption.

[BibT_eX]

[DOI]

Catherine Meadows

Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis, 2004

Sound Approximations to Diffie-Hellman Using Rewrite Rules.

[BibT_eX]

[DOI]

Catherine Meadows

Proceedings of the Information and Communications Security, 6th International Conference, 2004

Unsound Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Schematic Saturation for Decision and Unification Problems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Automatic Decidability.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Basic Syntactic Mutation.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

Goal-Directed E-Unification.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

Complexity of Linear Standard Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2001

Decidability and Complexity of Finitely Closable Linear Equational Theories.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

1999

Basic Completion with E-cycle Simplification.

[BibT_eX]

[DOI]

Christelle Scharff

Fundam. Informaticae, 1999

1998

Local Simplification.

[BibT_eX]

[DOI]

Inf. Comput., 1998

SOUR graphs for efficient completion.

[BibT_eX]

[DOI]

Polina Strogova

Discret. Math. Theor. Comput. Sci., 1998

The Unification Problem for One Relation Thue Systems.

[BibT_eX]

[DOI]

Proceedings of the Artificial Intelligence and Symbolic Computation, 1998

1997

Oriented Equational Logic Programming is Complete.

[BibT_eX]

[DOI]

J. Symb. Comput., 1997

Goal-Directed Completion Using SOUR Graphs.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

1996

Fine-Grained Concurrent Completion.

[BibT_eX]

[DOI]

Claude Kirchner

Christelle Scharff

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

PATCH Graphs: An Efficient Data Structure for Completion of Finitely Presented Groups.

[BibT_eX]

[DOI]

Polina Strogova

Proceedings of the Artificial Intelligence and Symbolic Mathematical Computation, 1996

1995

Basic Paramodulation

[BibT_eX]

[DOI]

Inf. Comput., September, 1995

Redundancy Criteria for Constrained Completion.

[BibT_eX]

[DOI]

Wayne Snyder

Theor. Comput. Sci., 1995

Paramodulation without Duplication

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1995

1992

Basic Paramodulation and Superposition.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Goal Directed Strategies for Paramodulation.

[BibT_eX]

[DOI]

Wayne Snyder

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

1990

An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality.

[BibT_eX]

[DOI]

Wayne Snyder