Expression reduction systems Z Khasidashvili Proceedings of I. Vekua Institute of Applied Mathematics 36, 200-220, 1990 | 74 | 1990 |

Optimal normalization in orthogonal term rewriting systems Z Khasidashvili International Conference on Rewriting Techniques and Applications, 243-258, 1993 | 46 | 1993 |

Encoding RTL constructs for MathSAT: a preliminary report M Bozzano, R Bruttomesso, A Cimatti, A Franzén, Z Hanna, ... Electronic Notes in Theoretical Computer Science 144 (2), 3-14, 2006 | 42 | 2006 |

Relative normalization in deterministic residual structures J Glauert, Z Khasidashvili Colloquium on Trees in Algebra and Programming, 180-195, 1996 | 35 | 1996 |

The Church-Rosser theorem in orthogonal combinatory reduction systems Z Khasidashvili | 35 | 1992 |

Relative normalization in orthogonal expression reduction systems J Glauert, Z Khasidashvili International Workshop on Conditional Term Rewriting Systems, 144-165, 1994 | 32 | 1994 |

The longest perpetual reductions in orthogonal expression reduction systems Z Khasidashvili International Symposium on Logical Foundations of Computer Science, 191-203, 1994 | 32 | 1994 |

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints Z Khasidashvili, M Skaba, D Kaiss, Z Hanna IEEE/ACM International Conference on Computer Aided Design, 2004. ICCAD-2004 …, 2004 | 31 | 2004 |

Industrial strength SAT-based alignability algorithm for hardware equivalence verification D Kaiss, M Skaba, Z Hanna, Z Khasidashvili Formal Methods in Computer Aided Design (FMCAD'07), 20-26, 2007 | 30 | 2007 |

β-reductions and β-developments of λ-terms with the least number of steps ZO Khasidashvili International Conference on Computer Logic, 105-111, 1988 | 28 | 1988 |

On higher order recursive program schemes Z Khasidashvili Colloquium on Trees in Algebra and Programming, 172-186, 1994 | 26 | 1994 |

Encoding industrial hardware verification problems into effectively propositional logic M Emmer, Z Khasidashvili, K Korovin, A Voronkov Formal Methods in Computer Aided Design, 137-144, 2010 | 25 | 2010 |

Context-sensitive conditional expression reduction systems Z Khasidashvili, V Van Oostrom Electronic Notes in Theoretical Computer Science 2, 167-176, 1995 | 25* | 1995 |

Perpetuality and uniform normalization in orthogonal rewrite systems Z Khasidashvili, M Ogawa, V Van Oostrom Information and Computation 164 (1), 118-151, 2001 | 23 | 2001 |

Uniform normalisation beyond orthogonality Z Khasidashvili, M Ogawa, V Van Oostrom International Conference on Rewriting Techniques and Applications, 122-136, 2001 | 22 | 2001 |

Discrete normalization and standardization in deterministic residual structures Z Khasidashvili, J Glauert International Conference on Algebraic and Logic Programming, 135-149, 1996 | 21 | 1996 |

Preprocessing techniques for first-order clausification K Hoder, Z Khasidashvili, K Korovin, A Voronkov 2012 Formal Methods in Computer-Aided Design (FMCAD), 44-51, 2012 | 19 | 2012 |

Simultaneous SAT-based model checking of safety properties Z Khasidashvili, A Nadel, A Palti, Z Hanna Haifa Verification Conference, 56-75, 2005 | 19 | 2005 |

Expression reduction systems and extensions: An overview J Glauert, D Kesner, Z Khasidashvili Processes, Terms and Cycles: Steps on the Road to Infinity, 496-553, 2005 | 18 | 2005 |

An enhanced cut-points algorithm in formal equivalence verification Z Khasidashvili, J Moondanos, D Kaiss, Z Hanna Sixth IEEE International High-Level Design Validation and Test Workshop, 171-176, 2001 | 17 | 2001 |