Konstantin Korovin

Publication Activity (10 Years)

Years Active: 2000-2024
Publications (10 Years): 36

Top Topics

Driven Learning

Modulo Theories

Quantifier Elimination

Linear Constraints

Top Venues

Publications

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)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
SMLP: Symbolic Machine Learning Prover. CAV (1) (2024)
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 (2024)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
SMLP: Symbolic Machine Learning Prover (User Manual). CoRR (2024)
Johannes Schoisswohl, Laura Kovács, Konstantin Korovin
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR (2024)
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 (2024)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
SMLP: Symbolic Machine Learning Prover. CoRR (2024)
Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
-complete decision procedure for non-linear constraints. Theor. Comput. Sci. 975 (2023)
Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban
Guiding an Instantiation Prover with Graph Neural Networks. LPAR (2023)
Edvard K. Holden, Konstantin Korovin
Graph Sequence Learning for Premise Selection. CoRR (2023)
Alexander H. Gower, Konstantin Korovin, Daniel Brunnsåker, Ievgeniia A. Tiukova, Ross D. King
: A First-Order Logic Framework for Automated Improvement of Metabolic Network Models Through Abduction. DS (2023)
Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl
Refining Unification with Abstraction. LPAR (2023)
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 (2023)
Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) (2023)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
Combining Constraint Solving and Bayesian Techniques for System Optimization. IJCAI (2022)
Kaled M. Alshmrany, Ahmed Bhayat, Franz Brauße, Lucas C. Cordeiro, Konstantin Korovin, Tom Melham, Mustafa A. Mustafa, Pierre Olivier, Giles Reger, Fedor Shmarov
Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. SecDev (2022)
André Duarte, Konstantin Korovin
Ground Joinability and Connectedness in the Superposition Calculus. IJCAR (2022)
Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. ISSTA (2022)
Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
Machine Learning Meets The Herbrand Universe. CoRR (2022)
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 (2021)
Edvard K. Holden, Konstantin Korovin
Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving. CICM (2021)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
Bayesian Optimisation with Formal Guarantees. CoRR (2021)
André Duarte, Konstantin Korovin
AC Simplifications and Closure Redundancies in the Superposition Calculus. TABLEAUX (2021)
Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. CADE (2021)
André Duarte, Konstantin Korovin
AC Simplifications and Closure Redundancies in the Superposition Calculus. CoRR (2021)
Evgeniy Glushankov, Konstantin Korovin, Ilya Gorobtsov, Igor Boyko, Dmitriy Kirik
Optimization of Fan-Beam Radiation Pattern of Cylindrical Phased Array. ICUMT (2021)
Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. FMCAD (2020)
André Duarte, Konstantin Korovin
Implementing Superposition in iProver (System Description). IJCAR (2) (2020)
Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
A CDCL-style calculus for solving non-linear constraints. CoRR (2019)
Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
A CDCL-Style Calculus for Solving Non-linear Constraints. FroCos (2019)
Julio César López-Hernández, Konstantin Korovin
An Abstraction-Refinement Framework for Reasoning with Large Theories. IJCAR (2018)
Andrzej Stanislaw Kucik, Konstantin Korovin
Premise selection with neural networks and distributed representation of features. CoRR (2018)
Julio César López-Hernández, Konstantin Korovin
Towards an Abstraction-Refinement Framework for Reasoning with Large Theories. IWIL@LPAR (2017)
Zurab Khasidashvili, Konstantin Korovin
Predicate Elimination for Preprocessing in First-Order Theorem Proving. SAT (2016)
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 (2016)
Zurab Khasidashvili, Konstantin Korovin, Dmitry Tsarkov
EPR-based k-induction with Counterexample Guided Abstraction Refinement. GCAI (2015)
Konstantin Korovin, Marek Kosta, Thomas Sturm
Towards Conflict-Driven Learning for Virtual Substitution. CASC (2014)
Konstantin Korovin, Marek Kosta, Thomas Sturm
Towards Conflict-Driven Learning for Virtual Substitution. SMT (2014)
Konstantin Korovin, Margus Veanes
Skolemization Modulo Theories. ICMS (2014)
Konstantin Korovin
Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning. Programming Logics (2013)
Konstantin Korovin
From Resolution and DPLL to Solving Arithmetic Constraints. FroCos (2013)
Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC (2013)
Nikolaj Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
Instantiations, Zippers and EPR Interpolation. LPAR (short papers) (2013)
Konstantin Korovin
Non-cyclic Sorts for First-Order Satisfiability. FroCos (2013)
Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov
EPR-Based Bounded Model Checking at Word Level. IJCAR (2012)
Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
Preprocessing techniques for first-order clausification. FMCAD (2012)
Konstantin Korovin, Andrei Voronkov
GoRRiLA and Hard Reality. Ershov Memorial Conference (2011)
Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
Implementing Conflict Resolution. Ershov Memorial Conference (2011)
Konstantin Korovin, Andrei Voronkov
Solving Systems of Linear Inequalities by Bound Propagation. CADE (2011)
Konstantin Korovin, Christoph Sticksel
Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. LPAR (Yogyakarta) (2010)
Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
Encoding industrial hardware verification problems into effectively propositional logic. FMCAD (2010)
Konstantin Korovin, Christoph Sticksel
iProver-Eq: An Instantiation-Based Theorem Prover with Equality. IJCAR (2010)
Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
Conflict Resolution. CP (2009)
Konstantin Korovin
Instantiation-Based Automated Reasoning: From Theory to Practice. CADE (2009)
Konstantin Korovin
iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). IJCAR (2008)
Konstantin Korovin, Andrei Voronkov
Integrating Linear Arithmetic into Superposition Calculus. CSL (2007)
Harald Ganzinger, Konstantin Korovin
Theory Instantiation. LPAR (2006)
Konstantin Korovin, Andrei Voronkov
Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS (2005)
Konstantin Korovin, Andrei Voronkov
Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. 6 (2) (2005)
Harald Ganzinger, Konstantin Korovin
Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL (2004)
Konstantin Korovin, Andrei Voronkov
Orienting Equalities with the Knuth-Bendix Order. LICS (2003)
Konstantin Korovin, Andrei Voronkov
Orienting rewrite rules with the Knuth-Bendix order. Inf. Comput. 183 (2) (2003)
Harald Ganzinger, Konstantin Korovin
New Directions in Instantiation-Based Theorem Proving. LICS (2003)
Konstantin Korovin, Andrei Voronkov
An AC-Compatible Knuth-Bendix Order. CADE (2003)
Konstantin Korovin, Andrei Voronkov
Knuth-Bendix constraint solving is NP-complete CoRR (2002)
Konstantin Korovin, Andrei Voronkov
The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. FSTTCS (2002)
Konstantin Korovin, Andrei Voronkov
Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. RTA (2001)
Konstantin Korovin, Andrei Voronkov
Knuth-Bendix Constraint Solving Is NP-Complete. ICALP (2001)
Konstantin Korovin, Andrei Voronkov
The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ARW (2000)
Konstantin Korovin, Andrei Voronkov
A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. LICS (2000)