Home Publications iProver iProver-ML SMLP KSMT Teaching PhD Contact
  1. Graph sequence learning for premise selection
    E. K. Holden, K. Korovin
    Journal of Symbolic Computation, pp. 24, vol. 128, 102376, 2025 [@Elsevier, @arXiv, bitex@dblp]
  2. Invariant neural architecture for learning term synthesis in instantiation proving
    J, Piepenbrock, J. Urban, K. Korovin, M. Olsak, T. Heskes, M. Janota
    Journal of Symbolic Computation, pp. 21, vol. 128, 102375, 2025 [@Elsevier, bibtex@dblp]
  3. SMLP: Symbolic Machine Learning Prover
    F. Brausse, Z. Khasidashvili and K. Korovin
    The 36th International Conference on Computer Aided Verification (CAV'24). 2024 [@Springer, @arXiv, bibtex@dblp]
  4. VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
    J. Schoisswohl, L. Kovacs, K. Korovin
    The 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'24) [@EasyChair, bibtex@dblp]
  5. ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST
    X. Li, K. Song, M. R. Gadelha, F. Brausse, R. S. Menezes, K. Korovin, L. C. Cordeiro
    [@arXiv, ], 2024
  6. ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution)
    R. S Menezes, M. Aldughaim, B. Farias, X. Li, E. Manino, F. Shmarov, K. Song, F. Brausse, M. R. Gadelha, N. Tihanyi, K. Korovin, L. C. Cordeiro
    TACAS'24, p. 376-380, 2024 [@Springer, bibtex@dblp]
  7. The Use of AI-Robotic Systems for Scientific Discovery
    A. H. Gower, K. Korovin, D. Brunnsaker, F. Kronstrom, G. K. Reder, I. A. Tiukova, R. S. Reiserer, J. P. Wikswo, R. D. King
    [@arXiv, bibtex@dblp], 2024
  8. The ksmt calculus is a δ-complete decision procedure for non-linear constraints
    F. Brausse, K. Korovin, M. Korovina and N. Th. Mueller
    Theoretical Computer Science, vol 975, Elsevier, 2023 [pdf, bibtex@dblp]
  9. LGEM+: A First-Order Logic Framework for Automated Improvement of Metabolic Network Models Through Abduction
    A. H. Gower, K. Korovin, D. Brunnsaker, I. A. Tiukova, R. D. King
    Proceedings of the 26th International Conference Discovery Science, DS'23, p. 628-643, LNCS vol. 14276, Springer, 2023 [pdf, bibtex@dblp]
  10. ALASCA: Reasoning in Quantified Linear Arithmetic
    K. Korovin, L. Kovacs, G. Reger, J. Schoisswohl, A. Voronkov
    Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23) [pdf, bibtex@dblp]
  11. Refining Unification with Abstraction
    A. Bhayat, K. Korovin, L. Kovacs, J. Schoisswohl
    Proceedings of the 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'23), p. 36-47, EPiC Series in Computing, EasyChair, 2023 [pdf, bibtex@dblp]
  12. Guiding an Instantiation Prover with Graph Neural Networks
    K. Chvalovsky, K. Korovin, J. Piepenbrock, J. Urban
    Proceedings of the 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'23), p. 112-123, EPiC Series in Computing, EasyChair, 2023 [pdf, bibtex@dblp]
  13. Combining Constraint Solving and Bayesian Techniques for System Optimization
    F. Brausse, Z. Khasidashvili and K. Korovin
    Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI'22), pp 1788--1794, 2022 [pdf, bibtex@dplb]
  14. Ground Joinability and Connectedness in the Superposition Calculus
    A. Duarte and K. Korovin
    The 11th International Joint Conference on Automated Reasoning (IJCAR'22), pp 169--187, LNCS vol. 13385, Springer, 2022
    Best Paper Award [pdf, bibtex@dplb]
  15. Machine Learning Meets The Herbrand Universe
    J. Piepenbrock, J. Urban, K. Korovin, M. Olsak, T. Heskes, M. Janota
    [arXiv, bibtex@dblp], 2022
  16. ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC
    F. Brausse, F. Shmarov, R. Menezes, M. R. Gadelha, K. Korovin, G. Reger, L. C. Cordeiro
    The 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'22), pp. 773--776, ACM, 2022, [pdf, bibtex@dblp]
  17. Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities
    K. Alshmrany, A. Bhayat, F. Brausse, L. Cordeiro, K. Korovin, T. Melham, M. A. Mustafa, P. Olivier, G. Reger, F. Shmarov
    IEEE Secure Development Conference (SecDev'2022) [pdf, bibtex@dblp]
  18. AC Simplifications and Closure Redundancies in the Superposition Calculus
    A. Duarte and K. Korovin
    TABLEAUX 2021, LNCS 12842, pp 200--217, Springer, 2021 [Springer Link, bibtex, arXiv version]
  19. Bayesian Optimisation with Formal Guarantees
    F. Brausse, Z. Khasidashvili, K. Korovin
    2021 [arxiv version, bibtex@dblp]
  20. The ksmt calculus is a δ-complete decision procedure for non-linear constraints.
    F. Brausse, K. Korovin, M. Korovina and N. Th. Mueller
    CADE 2021, pp 113-130, LNCS vol. 12699, Springer, [bibtex, pdf, arxiv version, sildes]
  21. Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving
    E. K. Holden and K. Korovin
    CICM 2021, LNCS vol 12833, pp 107--123, Springer, [Springer, pdf, bibtex]
  22. Towards a Hybrid Approach to Protect AgainstMemory Safety Vulnerabilities
    K. Alshmrany, A. Bhayat, L. Cordeiro, K. Korovin,T. Melham, M. A. Mustafa, P. Olivier, G. Reger, F. Shmarov
    [preprint TechRxiv], 2021
  23. Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation
    F. Brausse, Z. Khasidashvili and K. Korovin
    Formal Methods in Computer-Aided Design (FMCAD'20), [pdf, bib, video]
  24. Implementing Superposition in iProver (System Description)
    A. Duarte and K. Korovin
    The 10th International Joint Conference on Automated Reasoning (IJCAR'20), [full paper+appx, bib],
  25. A CDCL-style calculus for solving non-linear constraints
    F. Brausse, K. Korovin, M. Korovina and N. Th. Mueller
    Best Paper Award The 12th International Symposium on Frontiers of Combining Systems (FroCoS'19)
    LNCS, v11715, pp 131-148, Springer, 2019 [link], [pdf (arxiv), bib]
  26. SMAC and XGBoost your Theorem Prover
    E. K. Holden, K. Korovin
    The 4th Conference on Artificial Intelligence and Theorem Proving (AITP'19) [pdf, bib],
  27. Premise selection with neural networks and distributed representation of features
    A. S. Kucik, K. Korovin
    [arXiv, bibtex], 2018
  28. An Abstraction-Refinement Framework for Reasoning with Large Theories
    J. C. L. Hernandez, K. Korovin
    International Joint Conference on Automated Reasoning (IJCAR'18), LNCS, Springer, 2018, [pdf, bibtex@dblp]
  29. Towards an Abstraction-Refinement Framework for Reasoning with Large Theories
    J. C. L. Hernandez, K. Korovin
    IWIL@LPAR 2017, Kalpa Publications in Computing, EasyChair, [full paper; bibtex@dblp]
  30. Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA
    A. Currin, K. Korovin, M. Ababi, K. Roper, D. B. Kell, P. J. Day, R. D. King
    Journal of The Royal Society Interface, 2017 [full paper; bibtex]
  31. Predicate elimination for preprocessing in first-order theorem proving
    Z. Khasidashvili, K. Korovin
    Theory and Applications of Satisfiability Testing (SAT'16) LNCS, Springer [pdf bibtex@dblp]
  32. Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA
    A. Currin, K. Korovin, M. Ababi, K. Roper, D. B. Kell, P. J. Day, R. D. King
    2016, [arXiv; bibtex@dblp]
  33. EPR-based k-induction with Counterexample Guided Abstraction Refinement
    Z. Khasidashvili, K. Korovin and D. Tsarkov
    Global Conference on Artificial Intelligence (GCAI'15) [pdf, bibtex ]
  34. Towards Conflict-Driven Learning for Virtual Substitution
    K. Korovin, M. Kosta, T. Sturm
    Computer Algebra in Scientific Computing, (CASC'14), LNCS, Springer, 2014, [pdf; bibtex@dblp]
  35. Skolemization Modulo Theories
    K. Korovin and M. Veanes
    The 4th International Congress on Mathematical Software (ICMS'14) [pdf; bibtex@dblp]
  36. Instantiations, Zippers and EPR Interpolation
    N. Bjorner, A. Gurfinkel, K. Korovin, O. Lahav
    Logic for Programming, Artificial Intelligence and Reasoning, (LPAR'13) (short) [pdf bibtex]
  37. Non-cyclic sorts for first-order satisfiability
    K. Korovin,
    Frontiers of Combining Systems (FroCoS'13), LNCS, Springer, 2013, [pdf, bibtex]
  38. Bound Propagation for Arithmetic Reasoning in Vampire
    I. Dragan, K. Korovin, L. Kovacs, A. Voronkov
    International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, (SYNASC'13), IEEE, 2013, [pdf; bibtex]
  39. Inst-Gen -- A Modular Approach to Instantiation-Based Automated Reasoning
    K. Korovin
    Programming Logics, Essays in Memory of Harald Ganzinger, Springer, 2013 [pdf, bibtex@dblp]
  40. Preprocessing Techniques for First-Order Clausification
    K. Hoder, Z. Khasidashvili, K. Korovin, A. Voronkov
    Formal Methods in Computer-Aided Design (FMCAD'12), IEEE, 2012 [pdf, bibtex@dblp]
  41. EPR-Based Bounded Model Checking at Word Level
    M. Emmer, Z. Khasidashvili, K. Korovin, C. Sticksel, A. Voronkov
    International Joint Conference on Automated Reasoning, IJCAR 2012 [pdf; bibtex@dblp]
  42. A Note on Model Representation and Proof Extraction in the First-Order Instantiation-Based Calculus Inst-Gen,
    K. Korovin, C. Sticksel
    Automated Reasoning Workshop (ARW'12) [pdf, bib]
  43. Solving Systems of Linear Inequalities by Bound Propagation
    K. Korovin and A. Voronkov
    International Conference on Automated Deduction, (CADE'11), LNCS, Springer, 2011, [pdf, bibtex@dblp]
  44. Implementing Conflict Resolution
    K. Korovin, N. Tsiskaridze and A. Voronkov
    Perspectives of Systems Informatics (PSI'11), LNCS, Springer, 2011, [pdf; bibtex@dblp]
  45. GoRRiLA and Hard Reality
    K. Korovin and A. Voronkov
    Perspectives of Systems Informatics (PSI'11), LNCS, Springer, 2011, [pdf, bibtex@dblp]
  46. Encoding Industrial Hardware Verification Problems into Effectively Propositional Logic
    M. Emmer, Z. Khasidashvili, K. Korovin and A. Voronkov
    Formal Methods in Computer-Aided Design, (FMCAD'10), IEEE, 2010, [pdf, bibtex@dblp]
  47. Labelled Unit Superposition Calculi for Instantiation-based Reasoning
    K. Korovin and C.Sticksel
    Logic for Programming, Artificial Intelligence and Reasoning, (LPAR'10), LNCS, Springer, 2010, [pdf, bibtex@dblp]
  48. iProver-Eq: An Instantiation-based Theorem Prover with Equality
    K. Korovin and C.Sticksel
    International Joint Conference on Automated Reasoning, (IJCAR'10), LNCS, Springer, 2010, [pdf, bibtex@dblp]
  49. Conflict Resolution
    K. Korovin, N. Tsiskaridze, A. Voronkov
    Runner-up Best Paper Award
    International Conference on Principles and Practice of Constraint Programming, CP'09, LNCS, Springer, 2009, [pdf, bibtex@dblp]
  50. An Invitation to Instantiation-Based Reasoning: From Theory to Practice,
    K. Korovin
    Invited paper International Conference on Automated Deduction, (CADE'09), LNCS, Springer, 2009, [pdf, bib]
  51. iProver - An Instantiation-Based Theorem Prover for First-Order Logic
    K. Korovin
    International Joint Conference on Automated Reasoning, (IJCAR'08), LNCS, Springer, 2008, [pdf, bib]
  52. Integrating Linear Arithmetic into Superposition Calculus
    K. Korovin, A. Voronkov
    Computer Science Logic, (CSL'07), LNCS, Springer, 2007 [pdf, bib]
  53. Theory Instantiation
    H. Ganzinger, K. Korovin
    Logic for Programming, Artificial Intelligence and Reasoning, (LPAR'06), LNCS, Springer, 2006, [(full version) pdf, bib]
  54. Random Databases and Threshold for Monotone Non-Recursive Datalog
    K. Korovin, A. Voronkov
    International Symposium on Mathematical Foundations of Computer Science (MFCS'05), 2005, LNCS, Springer, [pdf, bibtex@dblp]
  55. Knuth-Bendix constraint solving is NP-complete
    K. Korovin, A. Voronkov
    ACM Transactions on Computational Logic 6(2): 361-388, 2005, [pdf, bibtex@dblp]
  56. Integrating equational reasoning into instantiation-based theorem proving
    H. Ganzinger, K. Korovin
    Computer Science Logic, (CSL'04), LNCS, Springer, 2004, [pdf, bibtex@dblp]
  57. New Directions in Instantiation-Based Theorem Proving
    H. Ganzinger, K. Korovin
    ACM/IEEE Symposium on Logic in Computer Science, (LICS'03), ACM, IEEE, 2003, [pdf bibtex@dblp]
  58. Orienting rewrite rules with the Knuth–Bendix order
    K. Korovin, A. Voronkov
    Journal Information and Computation, 2023, [pdf bibtex@dblp]
  59. Orienting Equalities with the Knuth-Bendix Order
    K. Korovin, A. Voronkov
    ACM/IEEE Symposium on Logic in Computer Science, (LICS'03), ACM, IEEE, 2003 [pdf bibtex@dblp]
  60. An AC-Compatible Knuth-Bendix Order
    K. Korovin, A. Voronkov
    International Conference on Automated Deduction (CADE'03), LNCS, Springer, 2003, [pdf bib] (Remark: There is a bug in the defenition of original non-ground AC-KBO in the case when the siganture contains zero-weight symbol f: in this case for each variable x, top(x) should be taken to be equal to f. Thanks to Akihisa Yamada for poiniting this out.)
  61. PhD thesis: Knuth-Bendix orders in automated deduction and term rewriting
    K. Korovin
    The University of Manchester, 2003 [pdf bib]
  62. The decidability of the first-order theory of the Knuth-Bendix order in the case of unary signatures
    K. Korovin, A. Voronkov
    Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02), LNCS, Springer, 2002, [pdf bibtex@dblp]
  63. Knuth-Bendix Constraint Solving Is NP-Complete
    K. Korovin, A. Voronkov
    The 28th International Colloquium on Automata, Languages and Programming, (ICALP'02), LNCS, Springer, 2002, [pdf, bibtex@dblp]
  64. Verifying orientability of rewrite rules using the Knuth-Bendix order
    K. Korovin, A. Voronkov
    The 12th International Conference on Rewriting Techniques and Applications (RTA'01), LNCS, Springer, [, bibtex@dblp]
  65. A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering
    K. Korovin, A. Voronkov
    ACM/IEEE Symposium on Logic in Computer Science, (LICS'00), ACM, IEEE, 2000, [pdf, bibtex@dblp]
  66. Compositions of permutations and algorithmic reducibilities
    K. Korovin
    Recursion Theory and Complexity, de Gruyter Series in Logic and Applications 2, 1999. [pdf bibtex@dblp ]
  67. Compositions of permutations and m-reducibility K. Korovin
    Notes: In this paper we show that for the m-reducibility for functions (which was introduced by M.Arslanov), there exists a r.e. set A such that the set of all permutations m-reducible to A is not closed under the composition.