```html Publications | Christopher Lynch

Publications

Christopher Lynch

Automated Reasoning | Theorem Proving | Formal Verification | Computational Logic

Publications

70+

Journal Articles, Conference Papers, and Technical Reports

1300+

Google Scholar Citations

31

Years of Publications

1995-2026

Publication Record

Professor Christopher Lynch has authored more than 70 publications spanning over three decades of research in automated reasoning, theorem proving, formal verification, computational logic, satisfiability modulo theories, unification theory, rewriting systems, and cryptographic protocol analysis. His work has received over 1,300 citations and has appeared in leading journals and conferences in automated deduction and symbolic computation, including the Journal of Automated Reasoning, Information and Computation, Theoretical Computer Science, CADE, IJCAR, FroCoS, ICTAC, and related venues.

For citation records and the most current publication information, please visit Christopher Lynch's Google Scholar profile .

Refereed Journal Publications

  1. Complete Trigger Selection in Satisfiability Modulo First-Order Theories, Christopher Lynch and Stephen Miner, arXiv preprint arXiv:2306.09436, 2023.
  2. CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms, D. Chichester, W. Du, R. Kauffman, H. Lin, C. Lynch, A. M. Marshall, et al., arXiv preprint arXiv:2209.10321, 2022.
  3. Congruence Closure Modulo Permutation Equations, Dongho Kim and Christopher Lynch, arXiv preprint arXiv:2109.03720, 2021.
  4. Bounded ACh Unification, Ajay Kumar and Christopher Lynch, Mathematical Structures in Computer Science, 30(6), 664-682, 2020.
  5. Efficient General AGH-Unification, Zhiqiang Liu and Christopher Lynch, Information and Computation, 238, 128-156, 2014.
  6. SMELS: Satisfiability Modulo Equality with Lazy Superposition, Christopher Lynch, Quang-Trung Ta, and Duc-Khanh Tran, Journal of Automated Reasoning, 51(3), 325-356, 2013.
  7. Unification Modulo Homomorphic Encryption, Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michal Rusinowitch, Journal of Automated Reasoning, 48(2), 135-158, 2012.
  8. Automatic Decidability and Combinability, Christopher Lynch, Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran, Information and Computation, 209(7), 1026-1047, 2011.
  9. On Deciding Satisfiability by Theorem Proving with Speculative Inferences, Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura, Journal of Automated Reasoning, 47(2), 161-189, 2011.
  10. Rewriting Interpolants, Christopher Lynch and Yuefeng Tang, Electronic Notes in Theoretical Computer Science, 212, 163-176, 2008.
  11. On the Relative Soundness of the Free Algebra Model for Public Key Encryption, Christopher Lynch and Catherine Meadows, Electronic Notes in Theoretical Computer Science, 125(1), 43-54, 2005.
  12. Local Simplification, Christopher Lynch, Information and Computation, 142(1), 102-126, 1998.
  13. SOUR Graphs for Efficient Completion, Christopher Lynch and Polina Strogova, Discrete Mathematics and Theoretical Computer Science, 2(1), 1-25, 1998.
  14. Oriented Equational Logic Programming is Complete, Christopher Lynch, Journal of Symbolic Computation, 23(1), 24-45, 1997.
  15. Redundancy Criteria for Constrained Completion, Christopher Lynch and Wayne Snyder, Theoretical Computer Science, 142(2), 141-177, 1995.
  16. Basic Paramodulation, Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder, Information and Computation, 121(2), 172-192, 1995.

Refereed Conference Publications

  1. Local XOR Unification: Definitions, Algorithms and Application to Cryptography, Hai Lin and Christopher Lynch, International Colloquium on Theoretical Aspects of Computing, pp. 272-289, 2022.
  2. Formal Analysis of Symbolic Authenticity, Hai Lin and Christopher Lynch, International Symposium on Frontiers of Combining Systems, pp. 271-286, 2021.
  3. Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems, Hai Lin, Christopher Lynch, A. M. Marshall, Catherine Meadows, Paliath Narendran, V. Ravishankar, et al., International Symposium on Frontiers of Combining Systems, pp. 253-270, 2021.
  4. Equational Theorem Proving Modulo, Dongho Kim and Christopher Lynch, International Conference on Automated Deduction, pp. 166-182, 2021.
  5. An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems, Dongho Kim and Christopher Lynch, 6th International Conference on Formal Structures for Computation and Deduction, 2021.
  6. Reviving Basic Narrowing Modulo, Dohan Kim, Christopher Lynch, and Paliath Narendran, International Symposium on Frontiers of Combining Systems, 313-329, 2019.
  7. On Asymmetric Unification for the Theory of XOR with a Homomorphism, Christopher Lynch, Andrew Marshall, Catherine Meadows, Paliath Narendran, and Veena Ravishankar, International Symposium on Frontiers of Combining Systems, 297-312, 2019.
  8. Finding Intruder Knowledge with Cap-Matching, Erin Hanna, Christopher Lynch, David Myers, and Corey Richardson, Foundations of Security, Protocols, and Equational Reasoning, 39-53, 2019.
  9. Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis, Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jose Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse, CADE, 231-248, 2013.
  10. On Forward Closure and the Finite Variant Property, Christopher Bouchard, Kimberly A. Gero, Christopher Lynch, and Paliath Narendran, FroCoS, 327-342, 2013.
  11. LIPIcs Volume 21, RTA 2013, Complete Volume, with F. van Raamsdonk, 24th International Conference on Rewriting Techniques and Applications, 2013.
  12. Constructing Bachmair-Ganzinger Models, Christopher Lynch, Programming Logics, 285-301, 2013.
  13. Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions, Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jose Meseguer, Paliath Narendran, Sonia Santiago, and Ralf Sasse, ESORICS, 73-90, 2012.
  14. Unification Modulo Synchronous Distributivity, Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, and Michal Rusinowitch, IJCAR, 14-29, 2012.
  15. Unification Modulo Theories of Blind Signatures, Serdar Erbatur, State University of New York at Albany, 2012.
  16. Efficient General Unification for XOR with Homomorphism, Zhiqiang Liu and Christopher Lynch, CADE, 407-421, 2011.
  17. Protocol Analysis in Maude-NPA Using Unification Modulo Homomorphic Encryption, Santiago Escobar, Deepak Kapur, Christopher Lynch, Catherine Meadows, Jose Meseguer, Paliath Narendran, and Ralf Sasse, PPDP, 2011.
  18. Cap Unification: Application to Protocol Security Modulo Homomorphic Encryption, Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michal Rusinowitch, ASIACCS, 2010.
  19. Unification Modulo Homomorphic Encryption, Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, and Michal Rusinowitch, FroCoS, 100-116, 2009.
  20. Combining Instance Generation and Resolution, Christopher Lynch and Ralph Eric McGregor, FroCoS, 304-318, 2009.
  21. On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving, Maria Paola Bonacina, Christopher Lynch, and Leonardo de Moura, CADE, 35-50, 2009.
  22. Equational and Cap Unification for Intrusion Analysis, Siva Anantharaman, Hai Lin, Paliath Narendran, Michael Rusinowitch, and Christopher Lynch, 2008.
  23. Interpolants for Linear Arithmetic in SMT, Christopher Lynch and Yuefeng Tang, ATVA, 2008.
  24. Protocol Verification via Rigid/Flexible Resolution, Stephanie Delaune, Hai Lin, and Christopher Lynch, LPAR, 2007.
  25. Encoding First Order Proofs in SAT, Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, and Christopher Lynch, CADE, 476-491, 2007.
  26. Automatic Decidability and Combinability Revisited, Christopher Lynch and Duc-Khanh Tran, CADE, 328-344, 2007.
  27. Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories, Christopher Lynch and Barbara Morawska, Rewriting Techniques and Applications, 90-104, 2005.
  28. Symbolic Debugging in Polynomial Time, Christopher Lynch and Barbara Morawska, 19th International Workshop on Unification, 2005.
  29. Sound Approximations to Diffie-Hellman Using Rewrite Rules, Christopher Lynch and Catherine Meadows, International Conference on Information and Communications Security, 262-277, 2004.
  30. Unsound Theorem Proving, Christopher Lynch, Computer Science Logic, 473-487, 2004.
  31. Automatic Decidability, Christopher Lynch and Barbara Morawska, LICS, 2002.
  32. Basic Syntactic Mutation, Christopher Lynch and Barbara Morawska, CADE, 2002.
  33. Automatic Decidability, Christopher Lynch and Barbara Morawska, LICS, 7-16, 2002.
  34. Complexity of Linear Standard Theories, Christopher Lynch and Barbara Morawska, LPAR, 188-200, 2001.
  35. Decidability and Complexity of Finitely Closable Linear Equational Theories, Christopher Lynch and Barbara Morawska, IJCAR, 495-513, 2001.
  36. Goal Directed E-Unification, Christopher Lynch and Barbara Morawska, RTA, 231-245, 2001.
  37. Approximating E-Unification, Christopher Lynch and Barbara Morawska, Workshop on Unification Theory, 2001.
  38. SOUR Graphs for Efficient Completion, Christopher Lynch and Polina Strogova, Discrete Mathematics and Theoretical Computer Science, 1998.
  39. Local Simplification Abstract, Christopher Lynch, Information and Computation, 1998.
  40. The Unification Problem for One Relation Thue Systems, Christopher Lynch, Artificial Intelligence and Symbolic Computation, 1998.
  41. Goal Directed Completion Using SOUR Graphs, Christopher Lynch, Rewriting Techniques and Applications, 1997.
  42. Goal Directed Completion Using SOUR Graphs Abstract, Christopher Lynch, 1997.
  43. Model Elimination Plus with Basic Ordered Paramodulation, Max Moser, Christopher Lynch, and Joachim Steinbach, draft, 1996.
  44. Model Elimination Plus with Basic Ordered Paramodulation Abstract, 1996.
  45. A Fine Grained Concurrent Completion Procedure, Claude Kirchner, Christopher Lynch, and Christelle Scharff, RTA, 1996.
  46. A Fine Grained Concurrent Completion Procedure Abstract, 1996.
  47. PATCH Graphs: An Efficient Data Structure for Completion of Finitely Presented Groups, Christopher Lynch and Polina Strogova, AISMC, 1996.
  48. PATCH Graphs Abstract, 1996.
  49. PATCH Graphs Long Version, 1996.
  50. Paramodulation Without Duplication, Christopher Lynch, LICS, 1995.
  51. Paramodulation Without Duplication Abstract, 1995.
  52. Redundancy Criteria for Constrained Completion, Christopher Lynch and Wayne Snyder, Theoretical Computer Science, 1995.
  53. Redundancy Criteria for Constrained Completion Abstract, 1995.
  54. Basic Paramodulation Abstract, Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder, 1995.
  55. Paramodulation Without Duplication, Christopher Lynch, LICS, 167-177, 1995.
  56. Model Elimination with Basic Ordered Paramodulation, Max Moser, Christopher Lynch, and Joachim Steinbach, Forschungsgruppe Automated Reasoning AR-95-11, 1995.

Navigation

Return to Christopher Lynch's homepage.

```