Author:Konstantin Korovin

Publications
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic (Extended Version) Johannes Schoisswohl, Laura Kovács and Konstantin Korovin EasyChair Preprint no. 13150
Refining Unification with Abstraction Ahmed Bhayat, Konstantin Korovin, Laura Kovács and Johannes Schoisswohl In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Guiding an Instantiation Prover with Graph Neural Networks Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock and Josef Urban In:Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
ALASCA: Reasoning in Quantified Linear Arithmetic (Extended Version) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl and Andrei Voronkov EasyChair Preprint no. 9606
ANDREI-60. Automated New-era Deductive Reasoning Event in Iberia Laura Kovács, Konstantin Korovin and Giles Reger (editors) EPiC Series in Computing, volume 68
LPAR-22 Workshop and Short Paper Proceedings Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe and Margus Veanes (editors) Kalpa Publications in Computing, volume 9
Towards an Abstraction-Refinement Framework for Reasoning with Large Theories Julio Cesar Lopez Hernandez and Konstantin Korovin In:IWIL Workshop and LPAR Short Presentations
EPR-based k-induction with Counterexample Guided Abstraction Refinement Zurab Khasidashvili, Konstantin Korovin and Dmitry Tsarkov In:GCAI 2015. Global Conference on Artificial Intelligence
UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification Santiago Escobar, Konstantin Korovin and Vladimir Rybakov (editors) EPiC Series in Computing, volume 24
Instantiations, Zippers and EPR Interpolation Nikolaj Bjorner, Arie Gurfinkel, Konstantin Korovin and Ori Lahav In:LPAR-19. 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
IWIL 2012. The 9th International Workshop on the Implementation of Logics Konstantin Korovin, Stephan Schulz and Eugenia Ternovska (editors) EPiC Series in Computing, volume 22
UNIF 2013. 27th International Workshop on Unification Konstantin Korovin and Barbara Morawska (editors) EPiC Series in Computing, volume 19

Keyphrases

abstraction refinement, arithmetic, automated reasoning², automated theorem proving, Bounded Model Checking, Clause Evaluation, Descision Procedure, EPR, EPR fragment, first-order logic, Graph Neural Networks, interpolation, k-induction, LIA, linear arithmetic², LIRA, logic, LRA, machine learning, Presburger arithmetic, Quantified First-Order Logic, quantifier elimination, SMT³, theorem proving³, unification, Unification with Abstraction.