| 2024 | CAV | SMLP: Symbolic Machine Learning Prover. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2024 | LPAR | VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. | Johannes Schoisswohl, Laura Kovcs, Konstantin Korovin |
| 2024 | TACAS | ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution). | Rafael S Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Braue, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro |
| 2023 | DIS | LGEM | Alexander H. Gower, Konstantin Korovin, Daniel Brunnsker, Ievgeniia A. Tiukova, Ross D. King |
| 2023 | LPAR | Refining Unification with Abstraction. | Ahmed Bhayat, Konstantin Korovin, Laura Kovcs, Johannes Schoisswohl |
| 2023 | LPAR | Guiding an Instantiation Prover with Graph Neural Networks. | Karel Chvalovsk, Konstantin Korovin, Jelle Piepenbrock, Josef Urban |
| 2023 | TACAS | ALASCA: Reasoning in Quantified Linear Arithmetic. | Konstantin Korovin, Laura Kovcs, Giles Reger, Johannes Schoisswohl, Andrei Voronkov |
| 2022 | CADE | Ground Joinability and Connectedness in the Superposition Calculus. | Andr Duarte, Konstantin Korovin |
| 2022 | IJCAI | Combining Constraint Solving and Bayesian Techniques for System Optimization. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2022 | ISSTA | ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. | Franz Braue, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro |
| 2021 | CADE | The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. | Franz Braue, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Mller |
| 2021 | TABLEAUX | AC Simplifications and Closure Redundancies in the Superposition Calculus. | Andr Duarte, Konstantin Korovin |
| 2020 | CADE | Implementing Superposition in iProver (System Description). | Andr Duarte, Konstantin Korovin |
| 2020 | FMCAD | Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. | Franz Braue, Zurab Khasidashvili, Konstantin Korovin |
| 2018 | CADE | An Abstraction-Refinement Framework for Reasoning with Large Theories. | Julio Csar Lpez-Hernndez, Konstantin Korovin |
| 2017 | LPAR | Towards an Abstraction-Refinement Framework for Reasoning with Large Theories. | Julio Csar Lpez-Hernndez, Konstantin Korovin |
| 2016 | SAT | Predicate Elimination for Preprocessing in First-Order Theorem Proving. | Zurab Khasidashvili, Konstantin Korovin |
| 2014 | CASC | Towards Conflict-Driven Learning for Virtual Substitution. | Konstantin Korovin, Marek Kosta, Thomas Sturm |
| 2013 | LPAR | Instantiations, Zippers and EPR Interpolation. | Nikolaj S. Bjrner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav |
| 2013 | SYNASC | Bound Propagation for Arithmetic Reasoning in Vampire. | Ioan Dragan, Konstantin Korovin, Laura Kovcs, Andrei Voronkov |
| 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 |
| 2011 | CADE | Solving Systems of Linear Inequalities by Bound Propagation. | Konstantin Korovin, Andrei Voronkov |
| 2010 | CADE | iProver-Eq: An Instantiation-Based Theorem Prover with Equality. | Konstantin Korovin, Christoph Sticksel |
| 2010 | FMCAD | Encoding industrial hardware verification problems into effectively propositional logic. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2010 | LPAR | Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. | Konstantin Korovin, Christoph Sticksel |
| 2009 | CADE | Instantiation-Based Automated Reasoning: From Theory to Practice. | Konstantin Korovin |
| 2009 | CP | Conflict Resolution. | Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov |
| 2008 | CADE | iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). | Konstantin Korovin |
| 2007 | CSL | Integrating Linear Arithmetic into Superposition Calculus. | Konstantin Korovin, Andrei Voronkov |
| 2006 | LPAR | Theory Instantiation. | Harald Ganzinger, Konstantin Korovin |
| 2005 | MFCS | Random Databases and Threshold for Monotone Non-recursive Datalog. | Konstantin Korovin, Andrei Voronkov |
| 2004 | CSL | Integrating Equational Reasoning into Instantiation-Based Theorem Proving. | Harald Ganzinger, Konstantin Korovin |
| 2003 | CADE | An AC-Compatible Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2003 | LICS | New Directions in Instantiation-Based Theorem Proving. | Harald Ganzinger, Konstantin Korovin |
| 2003 | LICS | Orienting Equalities with the Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2001 | ICALP | Knuth-Bendix Constraint Solving Is NP-Complete. | Konstantin Korovin, Andrei Voronkov |
| 2000 | LICS | A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. | Konstantin Korovin, Andrei Voronkov |