default search action
Konstantin Korovin
Person information
- affiliation: University of Manchester, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2025
- [j5]Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota:
Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. 128: 102375 (2025) - [j4]Edvard K. Holden, Konstantin Korovin:
Graph sequence learning for premise selection. J. Symb. Comput. 128: 102376 (2025) - 2024
- [c53]Franz Brauße
, Zurab Khasidashvili
SMLP: Symbolic Machine Learning Prover. CAV (1) 2024: 219-233 - [c52]Johannes Schoisswohl, Laura Kovács, Konstantin Korovin:
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR 2024: 147-164 - [c51]Rafael Sá Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro:
ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution). TACAS (3) 2024: 376-380 - [i15]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
SMLP: Symbolic Machine Learning Prover. CoRR abs/2402.01415 (2024) - [i14]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
SMLP: Symbolic Machine Learning Prover (User Manual). CoRR abs/2405.10215 (2024) - [i13]Alexander H. Gower, Konstantin Korovin, Daniel Brunnsåker, Filip Kronström, Gabriel K. Reder, Ievgeniia A. Tiukova, Ronald S. Reiserer, John P. Wikswo, Ross D. King:
The Use of AI-Robotic Systems for Scientific Discovery. CoRR abs/2406.17835 (2024) - [i12]Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Konstantin Korovin, Lucas C. Cordeiro:
ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST. CoRR abs/2406.17862 (2024) - [i11]Ievgeniia A. Tiukova, Daniel Brunnsåker, Erik Y. Bjurström, Alexander H. Gower, Filip Kronström, Gabriel K. Reder, Ronald S. Reiserer, Konstantin Korovin, Larisa N. Soldatova, John P. Wikswo, Ross D. King:
Genesis: Towards the Automation of Systems Biology Research. CoRR abs/2408.10689 (2024) - 2023
- [j3]Franz Brauße
The ksmt calculus is a δ-complete decision procedure for non-linear constraints. Theor. Comput. Sci. 975: 114125 (2023) - [c50]Alexander H. Gower
LGEM+: A First-Order Logic Framework for Automated Improvement of Metabolic Network Models Through Abduction. DS 2023: 628-643 - [c49]Ahmed Bhayat
Refining Unification with Abstraction. LPAR 2023: 36-47 - [c48]Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban:
Guiding an Instantiation Prover with Graph Neural Networks. LPAR 2023: 112-123 - [c47]Konstantin Korovin
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) 2023: 647-665 - [i10]Edvard K. Holden, Konstantin Korovin:
Graph Sequence Learning for Premise Selection. CoRR abs/2303.15642 (2023) - [i9]Rafael Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brauße, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro:
ESBMC v7.4: Harnessing the Power of Intervals. CoRR abs/2312.14746 (2023) - 2022
- [c46]André Duarte
Ground Joinability and Connectedness in the Superposition Calculus. IJCAR 2022: 169-187 - [c45]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
Combining Constraint Solving and Bayesian Techniques for System Optimization. IJCAI 2022: 1788-1794 - [c44]Franz Brauße, Fedor Shmarov, Rafael Menezes
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. ISSTA 2022: 773-776 - [c43]Kaled M. Alshmrany
Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. SecDev 2022: 52-58 - [i8]Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota:
Machine Learning Meets The Herbrand Universe. CoRR abs/2210.03590 (2022) - 2021
- [c42]Franz Brauße
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. CADE 2021: 113-130 - [c41]Evgeniy Glushankov, Konstantin Korovin, Ilya Gorobtsov
Optimization of Fan-Beam Radiation Pattern of Cylindrical Phased Array. ICUMT 2021: 224-229 - [c40]Edvard K. Holden
Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving. CICM 2021: 107-123 - [c39]André Duarte
AC Simplifications and Closure Redundancies in the Superposition Calculus. TABLEAUX 2021: 200-217 - [i7]Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller:
The ksmt calculus is a δ-complete decision procedure for non-linear constraints. CoRR abs/2104.13269 (2021) - [i6]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
Bayesian Optimisation with Formal Guarantees. CoRR abs/2106.06067 (2021) - [i5]André Duarte
AC Simplifications and Closure Redundancies in the Superposition Calculus. CoRR abs/2107.08409 (2021) - 2020
- [c38]André Duarte
Implementing Superposition in iProver (System Description). IJCAR (2) 2020: 388-397 - [c37]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. FMCAD 2020: 119-127 - [e5]Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret:
Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual). CEUR Workshop Proceedings 2752, CEUR-WS.org 2020 [contents]
2010 – 2019
- 2019
- [c36]Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller:
A CDCL-Style Calculus for Solving Non-linear Constraints. FroCos 2019: 131-148 - [i4]Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller:
A CDCL-style calculus for solving non-linear constraints. CoRR abs/1905.09227 (2019) - 2018
- [c35]Julio César López-Hernández, Konstantin Korovin:
An Abstraction-Refinement Framework for Reasoning with Large Theories. IJCAR 2018: 663-679 - [e4]Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes:
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018. Kalpa Publications in Computing 9, EasyChair 2018 [contents] - [i3]Andrzej Stanislaw Kucik
Premise selection with neural networks and distributed representation of features. CoRR abs/1807.10268 (2018) - 2017
- [c34]Julio César López-Hernández, Konstantin Korovin:
Towards an Abstraction-Refinement Framework for Reasoning with Large Theories. IWIL@LPAR 2017: 119-123 - 2016
- [c33]Zurab Khasidashvili, Konstantin Korovin:
Predicate Elimination for Preprocessing in First-Order Theorem Proving. SAT 2016: 361-372 - [i2]Andrew Currin, Konstantin Korovin, Maria Ababi, Katherine Roper, Douglas B. Kell, Philip J. Day, Ross D. King:
Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA. CoRR abs/1607.08078 (2016) - 2015
- [c32]Zurab Khasidashvili, Konstantin Korovin, Dmitry Tsarkov:
EPR-based k-induction with Counterexample Guided Abstraction Refinement. GCAI 2015: 137-150 - 2014
- [c31]Konstantin Korovin, Marek Kosta, Thomas Sturm
Towards Conflict-Driven Learning for Virtual Substitution. CASC 2014: 256-270 - [c30]Konstantin Korovin, Margus Veanes:
Skolemization Modulo Theories. ICMS 2014: 303-306 - [c29]Konstantin Korovin, Marek Kosta, Thomas Sturm:
Towards Conflict-Driven Learning for Virtual Substitution. SMT 2014: 71 - [e3]Santiago Escobar, Konstantin Korovin, Vladimir V. Rybakov:
UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification, Manchester, UK, July 1, 2012. EPiC Series in Computing 24, EasyChair 2014 [contents] - 2013
- [c28]Konstantin Korovin:
Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning. Programming Logics 2013: 239-270 - [c27]Konstantin Korovin:
Non-cyclic Sorts for First-Order Satisfiability. FroCos 2013: 214-228 - [c26]Konstantin Korovin:
From Resolution and DPLL to Solving Arithmetic Constraints. FroCos 2013: 261-262 - [c25]Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav:
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) 2013: 35-41 - [c24]Ioan Dragan
Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC 2013: 169-176 - [e2]Konstantin Korovin, Stephan Schulz, Eugenia Ternovska:
IWIL 2012: The 9th International Workshop on the Implementation of Logics, Merida, Venezuela, March 10, 2012. EPiC Series in Computing 22, EasyChair 2013 [contents] - [e1]Konstantin Korovin, Barbara Morawska:
27th International Workshop on Unification, UNIF 2013, Eindhoven, Netherlands, June 26, 2013. EPiC Series in Computing 19, EasyChair 2013 [contents] - 2012
- [c23]Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov:
EPR-Based Bounded Model Checking at Word Level. IJCAR 2012: 210-224 - [c22]Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov:
Preprocessing techniques for first-order clausification. FMCAD 2012: 44-51 - 2011
- [c21]Konstantin Korovin, Andrei Voronkov:
Solving Systems of Linear Inequalities by Bound Propagation. CADE 2011: 369-383 - [c20]Konstantin Korovin, Andrei Voronkov:
GoRRiLA and Hard Reality. Ershov Memorial Conference 2011: 243-250 - [c19]Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov:
Implementing Conflict Resolution. Ershov Memorial Conference 2011: 362-376 - 2010
- [c18]Konstantin Korovin, Christoph Sticksel:
iProver-Eq: An Instantiation-Based Theorem Prover with Equality. IJCAR 2010: 196-202 - [c17]Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov:
Encoding industrial hardware verification problems into effectively propositional logic. FMCAD 2010: 137-144 - [c16]Konstantin Korovin, Christoph Sticksel:
Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. LPAR (Yogyakarta) 2010: 459-473
2000 – 2009
- 2009
- [c15]Konstantin Korovin:
Instantiation-Based Automated Reasoning: From Theory to Practice. CADE 2009: 163-166 - [c14]Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov:
Conflict Resolution. CP 2009: 509-523 - 2008
- [c13]Konstantin Korovin:
iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). IJCAR 2008: 292-298 - 2007
- [c12]Konstantin Korovin, Andrei Voronkov:
Integrating Linear Arithmetic into Superposition Calculus. CSL 2007: 223-237 - 2006
- [c11]Harald Ganzinger, Konstantin Korovin:
Theory Instantiation. LPAR 2006: 497-511 - 2005
- [j2]Konstantin Korovin, Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. 6(2): 361-388 (2005) - [c10]Konstantin Korovin, Andrei Voronkov:
Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS 2005: 591-602 - 2004
- [c9]Harald Ganzinger, Konstantin Korovin:
Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL 2004: 71-84 - 2003
- [j1]Konstantin Korovin, Andrei Voronkov:
Orienting rewrite rules with the Knuth-Bendix order. Inf. Comput. 183(2): 165-186 (2003) - [c8]Konstantin Korovin, Andrei Voronkov:
An AC-Compatible Knuth-Bendix Order. CADE 2003: 47-59 - [c7]Harald Ganzinger, Konstantin Korovin:
New Directions in Instantiation-Based Theorem Proving. LICS 2003: 55-64 - [c6]Konstantin Korovin, Andrei Voronkov:
Orienting Equalities with the Knuth-Bendix Order. LICS 2003: 75- - 2002
- [c5]Konstantin Korovin, Andrei Voronkov:
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. FSTTCS 2002: 230-240 - [i1]Konstantin Korovin, Andrei Voronkov:
Knuth-Bendix constraint solving is NP-complete. CoRR cs.LO/0207068 (2002) - 2001
- [c4]Konstantin Korovin, Andrei Voronkov:
Knuth-Bendix Constraint Solving Is NP-Complete. ICALP 2001: 979-992 - [c3]Konstantin Korovin, Andrei Voronkov:
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. RTA 2001: 137-153 - 2000
- [c2]Konstantin Korovin, Andrei Voronkov:
The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ARW 2000 - [c1]Konstantin Korovin, Andrei Voronkov:
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. LICS 2000: 291-302
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-12-10 20:49 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: