beta-reductions and beta developments of lambda terms with the least number of steps. - Zurab Khasidashvili (Conference on Computer Logic, 1988)

On the Equivalence of Persistent Term Rewriting Systems and Recursive Program Schemes. - Zurab Khasidashvili (ISTCS, 1993)

Optimal Normalization in Orthogonal Term Rewriting Systems. - Zurab Khasidashvili (RTA, 1993)

On Higher Order Recursive Program Schemes. - Zurab Khasidashvili (CAAP, 1994)

Relative Normalization in Orthogonal Expression Reduction Systems. - John R. W. Glauert; Zurab Khasidashvili (CTRS, 1994)

Perpetuality and Strong Normalization in Orthogonal Term Rewriting Systems. - Zurab Khasidashvili (STACS, 1994)

Context-sensitive conditional expression reduction systems. - Zurab Khasidashvili; Vincent van Oostrom (SEGRAGRA, 1995)

Discrete Normalization and Standardization in Deterministic Residual Structures. - Zurab Khasidashvili; John R. W. Glauert (ALP, 1996)

Relative Normalization in Deterministic Residual Structures. - John R. W. Glauert; Zurab Khasidashvili (CAAP, 1996)

Minimal Relative Normalization in Orthogonal Expression Reduction Systems. - John R. W. Glauert; Zurab Khasidashvili (FSTTCS, 1996)

Perpetuality and Uniform Normalization. - Zurab Khasidashvili; Mizuhito Ogawa (ALP/HOA, 1997)

The Geometry of Orthogonal Reduction Spaces. - Zurab Khasidashvili; John R. W. Glauert (ICALP, 1997)

Relating Conflict-Free Stable Transition and Event Models (Extended Abstract). - Zurab Khasidashvili; John R. W. Glauert (MFCS, 1997)

Normalization of Typable Terms by Superdevelopments. - Zurab Khasidashvili; Adolfo Piperno (CSL, 1998)

Stable results and relative normalization. - John R. W. Glauert; Richard Kennaway; Zurab Khasidashvili (J. Log. Comput., 2000)

A syntactical analysis of normalization. - Zurab Khasidashvili; Adolfo Piperno (J. Log. Comput., 2000)

An enhanced cut-points algorithm in formal equivalence verification. - Zurab Khasidashvili; John Moondanos; Daher Kaiss; Ziyad Hanna (HLDVT, 2001)

Uniform Normalisation beyond Orthogonality. - Zurab Khasidashvili; Mizuhito Ogawa; Vincent van Oostrom (RTA, 2001)

Perpetuality and Uniform Normalization in Orthogonal Rewrite Systems. - Zurab Khasidashvili; Mizuhito Ogawa; Vincent van Oostrom (Inf. Comput., 2001)

On the longest perpetual reductions in orthogonal expression reduction systems. - Zurab Khasidashvili (Theor. Comput. Sci., 2001)

TRANS: efficient sequential verification of loop-free circuits. - Zurab Khasidashvili; John Moondanos; Ziyad Hanna (HLDVT, 2002)

Static Analysis of Modularity of beta-Reduction in the Hyperbalanced lambda-Calculus. - Richard Kennaway; Zurab Khasidashvili; Adolfo Piperno (RTA, 2002)

An Abstract Böhm-normalization. - John R. W. Glauert; Zurab Khasidashvili (WRS, 2002)

Relating conflict-free stable transition and event models via redex families. - Zurab Khasidashvili; John R. W. Glauert (Theor. Comput. Sci., 2002)

Stable Computational Semantics of Conflict-Free Rewrite Systems (Partial Orders with Duplication). - Zurab Khasidashvili; John R. W. Glauert (RTA, 2003)

An Abstract Concept of Optimal Implementation. - Zurab Khasidashvili; John R. W. Glauert (WRS, 2003)

SAT-based methods for sequential hardware equivalence verification without synchronization. - Zurab Khasidashvili; Ziyad Hanna (BMC@CAV, 2003)

Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. - Zurab Khasidashvili; Marcelo Skaba; Daher Kaiss; Ziyad Hanna (ICCAD, 2004)

Expression Reduction Systems and Extensions: An Overview. - John R. W. Glauert; Delia Kesner; Zurab Khasidashvili (Processes, Terms and Cycles, 2005)

Simultaneous SAT-Based Model Checking of Safety Properties. - Zurab Khasidashvili; Alexander Nadel; Amit Palti; Ziyad Hanna (Haifa Verification Conference, 2005)

Encoding RTL Constructs for MathSAT: a Preliminary Report. - Marco Bozzano; Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Ziyad Hanna; Zurab Khasidashvili; Amit Palti; Roberto Sebastiani (PDPAR@CAV, 2005)

The conflict-free Reduction Geometry. - Zurab Khasidashvili; John R. W. Glauert (Theor. Comput. Sci., 2005)

Post-reboot Equivalence and Compositional Verification of Hardware. - Zurab Khasidashvili; Marcelo Skaba; Daher Kaiss; Ziyad Hanna (FMCAD, 2006)

Seqver : A Sequential Equivalence Verifier for Hardware Designs . - Daher Kaiss; Silvian Goldenberg; Zurab Khasidashvili (ICCD, 2006)

Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. - Daher Kaiss; Marcelo Skaba; Ziyad Hanna; Zurab Khasidashvili (FMCAD, 2007)

On Formal Equivalence Verification of Hardware. - Zurab Khasidashvili (CSR, 2008)

Assume-guarantee validation for STE properties within an SVA environment. - Zurab Khasidashvili; Gavriel Gavrielov; Tom Melham (FMCAD, 2009)

A compositional theory for post-reboot observational equivalence checking of hardware. - Zurab Khasidashvili; Daher Kaiss; Doron Bustan (FMCAD, 2009)

Verifying equivalence of memories using a first order logic theorem prover. - Zurab Khasidashvili; Mahmoud Kinanah; Andrei Voronkov (FMCAD, 2009)

Encoding industrial hardware verification problems into effectively propositional logic. - Moshe Emmer; Zurab Khasidashvili; Konstantin Korovin; Andrei Voronkov (FMCAD, 2010)

Implicative Simultaneous Satisfiability and Applications. - Zurab Khasidashvili; Alexander Nadel (Haifa Verification Conference, 2011)

EPR-Based Bounded Model Checking at Word Level. - Moshe Emmer; Zurab Khasidashvili; Konstantin Korovin; Christoph Sticksel; Andrei Voronkov (IJCAR, 2012)

Preprocessing techniques for first-order clausification. - Krystof Hoder; Zurab Khasidashvili; Konstantin Korovin; Andrei Voronkov (FMCAD, 2012)

From visual to logical formalisms for SoC validation. - Ranan Fraer; Doron Keren; Zurab Khasidashvili; Alexander Novakovsky; Avi Puder; Eli Singerman; Eran Talmor; Moshe Y. Vardi; Jin Yang 006 (MEMOCODE, 2014)

Word-Level Symbolic Trajectory Evaluation. - Supratik Chakraborty; Zurab Khasidashvili; Carl-Johan H. Seger; Rajkumar Gajavelly; Tanmay Haldankar; Dinesh Chhatani; Rakesh Mistry (CAV (2), 2015)

EPR-based k-induction with Counterexample Guided Abstraction Refinement. - Zurab Khasidashvili; Konstantin Korovin; Dmitry Tsarkov (GCAI, 2015)

Predicate Elimination for Preprocessing in First-Order Theorem Proving. - Zurab Khasidashvili; Konstantin Korovin (SAT, 2016)

Symbolic trajectory evaluation for word-level verification: theory and implementation. - Supratik Chakraborty; Zurab Khasidashvili; Carl-Johan H. Seger; Rajkumar Gajavelly; Tanmay Haldankar; Dinesh Chhatani; Rakesh Mistry (Formal Methods Syst. Des., 2017)

Range Analysis and Applications to Root Causing. - Zurab Khasidashvili; Adam J. Norman (DSAA, 2019)

Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. - Franz Brauße; Zurab Khasidashvili; Konstantin Korovin (FMCAD, 2020)

Bayesian Optimisation with Formal Guarantees. - Franz Brauße; Zurab Khasidashvili; Konstantin Korovin (CoRR, 2021)

Feature range analysis. - Zurab Khasidashvili; Adam J. Norman (Int. J. Data Sci. Anal., 2021)

Combining Constraint Solving and Bayesian Techniques for System Optimization. - Franz Brauße; Zurab Khasidashvili; Konstantin Korovin (IJCAI, 2022)

Accelerating System-Level Debug Using Rule Learning and Subgroup Discovery Techniques. - Zurab Khasidashvili (CoRR, 2022)

SMLP: Symbolic Machine Learning Prover. - Franz Brauße; Zurab Khasidashvili; Konstantin Korovin (CAV (1), 2024)

SMLP: Symbolic Machine Learning Prover (User Manual). - Franz Brauße; Zurab Khasidashvili; Konstantin Korovin (CoRR, 2024)