| 2024 | CAV | SMLP: Symbolic Machine Learning Prover. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2022 | IJCAI | Combining Constraint Solving and Bayesian Techniques for System Optimization. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2020 | FMCAD | Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2019 | DSAA | Range Analysis and Applications to Root Causing. | Zurab Khasidashvili, Adam J. Norman |
| 2016 | SAT | Predicate Elimination for Preprocessing in First-Order Theorem Proving. | Zurab Khasidashvili, Konstantin Korovin |
| 2015 | CAV | Word-Level Symbolic Trajectory Evaluation. | Supratik Chakraborty, Zurab Khasidashvili, Carl-Johan H. Seger, Rajkumar Gajavelly, Tanmay Haldankar, Dinesh Chhatani, Rakesh Mistry |
| 2014 | MEMOCODE | 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 |
| 2012 | CADE | EPR-Based Bounded Model Checking at Word Level. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov |
| 2012 | FMCAD | Preprocessing techniques for first-order clausification. | Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2010 | FMCAD | Encoding industrial hardware verification problems into effectively propositional logic. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2009 | FMCAD | Assume-guarantee validation for STE properties within an SVA environment. | Zurab Khasidashvili, Gavriel Gavrielov, Tom Melham |
| 2009 | FMCAD | A compositional theory for post-reboot observational equivalence checking of hardware. | Zurab Khasidashvili, Daher Kaiss, Doron Bustan |
| 2009 | FMCAD | Verifying equivalence of memories using a first order logic theorem prover. | Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |
| 2008 | CSR | On Formal Equivalence Verification of Hardware. | Zurab Khasidashvili |
| 2007 | FMCAD | Industrial Strength SAT-based Alignability Algorithm for Hardware Equivalence Verification. | Daher Kaiss, Marcelo Skaba, Ziyad Hanna, Zurab Khasidashvili |
| 2006 | FMCAD | Post-reboot Equivalence and Compositional Verification of Hardware. | Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna |
| 2006 | ICCD | Seqver : A Sequential Equivalence Verifier for Hardware Designs . | Daher Kaiss, Silvian Goldenberg, Zurab Khasidashvili |
| 2004 | ICCAD | Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. | Zurab Khasidashvili, Marcelo Skaba, Daher Kaiss, Ziyad Hanna |
| 1998 | CSL | Normalization of Typable Terms by Superdevelopments. | Zurab Khasidashvili, Adolfo Piperno |
| 1997 | ICALP | The Geometry of Orthogonal Reduction Spaces. | Zurab Khasidashvili, John R. W. Glauert |
| 1997 | MFCS | Relating Conflict-Free Stable Transition and Event Models (Extended Abstract). | Zurab Khasidashvili, John R. W. Glauert |
| 1994 | LFCS | The Longest Perpetual Reductions in Orthogonal Expression Reduction Systems. | Zurab Khasidashvili |
| 1994 | STACS | Perpetuality and Strong Normalization in Orthogonal Term Rewriting Systems. | Zurab Khasidashvili |