Konstantin Korovin

79 papers A* 5A 12B 13C 1Misc 1Journal 21Unranked 21

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	ESBMC v7.6: Enhanced model checking of C++ programs with clang AST. Sci. Comput. Program. Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Konstantin Korovin, Lucas C. Cordeiro
2025	J	`jnl`	Graph sequence learning for premise selection. J. Symb. Comput. Edvard K. Holden, Konstantin Korovin
2025	J	`jnl`	Invariant neural architecture for learning term synthesis in instantiation proving. J. Symb. Comput. Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolás Janota
2024	—	`conf`	ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution). TACAS (3) 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
2024	J	`jnl`	ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST. CoRR Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Konstantin Korovin, Lucas C. Cordeiro
2024	J	`jnl`	Genesis: Towards the Automation of Systems Biology Research. CoRR 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
2024	J	`jnl`	SMLP: Symbolic Machine Learning Prover (User Manual). CoRR Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2024	—	`conf`	SMLP: Symbolic Machine Learning Prover. CAV (1) Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2024	J	`jnl`	SMLP: Symbolic Machine Learning Prover. CoRR Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2024	J	`jnl`	The Use of AI-Robotic Systems for Scientific Discovery. CoRR 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
2024	B	`conf`	VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR Johannes Schoisswohl, Laura Kovács, Konstantin Korovin
2023	—	`conf`	ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov
2023	J	`jnl`	ESBMC v7.4: Harnessing the Power of Intervals. CoRR 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
2023	J	`jnl`	Graph Sequence Learning for Premise Selection. CoRR Edvard K. Holden, Konstantin Korovin
2023	B	`conf`	Guiding an Instantiation Prover with Graph Neural Networks. LPAR Karel Chvalovský, Konstantin Korovin, Jelle Piepenbrock, Josef Urban
2023	B	`conf`	LGEM DS Alexander H. Gower, Konstantin Korovin, Daniel Brunnsåker, Ievgeniia A. Tiukova, Ross D. King
2023	B	`conf`	Refining Unification with Abstraction. LPAR Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl
2023	J	`jnl`	The ksmt calculus is a Theor. Comput. Sci. Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
2022	A*	`conf`	Combining Constraint Solving and Bayesian Techniques for System Optimization. IJCAI Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2022	A	`conf`	ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. ISSTA Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro
2022	A	`conf`	Ground Joinability and Connectedness in the Superposition Calculus. IJCAR André Duarte, Konstantin Korovin
2022	J	`jnl`	Machine Learning Meets The Herbrand Universe. CoRR Jelle Piepenbrock, Josef Urban, Konstantin Korovin, Miroslav Olsák, Tom Heskes, Mikolas Janota
2022	—	`conf`	Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities. SecDev Kaled M. Alshmrany, Ahmed Bhayat, Franz Brauße, Lucas C. Cordeiro, Konstantin Korovin, Tom Melham, Mustafa A. Mustafa, Pierre Olivier, Giles Reger, Fedor Shmarov
2021	B	`conf`	AC Simplifications and Closure Redundancies in the Superposition Calculus. TABLEAUX André Duarte, Konstantin Korovin
2021	J	`jnl`	AC Simplifications and Closure Redundancies in the Superposition Calculus. CoRR André Duarte, Konstantin Korovin
2021	J	`jnl`	Bayesian Optimisation with Formal Guarantees. CoRR Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2021	C	`conf`	Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving. CICM Edvard K. Holden, Konstantin Korovin
2021	—	`conf`	Optimization of Fan-Beam Radiation Pattern of Cylindrical Phased Array. ICUMT Evgeniy Glushankov, Konstantin Korovin, Ilya Gorobtsov, Igor Boyko, Dmitriy Kirik
2021	A	`conf`	The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. CADE Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
2021	J	`jnl`	The ksmt calculus is a δ-complete decision procedure for non-linear constraints. CoRR Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
2020	—	`conf`	Implementing Superposition in iProver (System Description). IJCAR (2) André Duarte, Konstantin Korovin
2020	—	`ed.`	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). PAAR+SC²@IJCAR Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret
2020	B	`conf`	Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation. FMCAD Franz Brauße, Zurab Khasidashvili, Konstantin Korovin
2019	—	`conf`	A CDCL-Style Calculus for Solving Non-linear Constraints. FroCos Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
2019	J	`jnl`	A CDCL-style calculus for solving non-linear constraints. CoRR Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller
2018	A	`conf`	An Abstraction-Refinement Framework for Reasoning with Large Theories. IJCAR Julio César López-Hernández, Konstantin Korovin
2018	—	`ed.`	LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018 LPAR (Workshop and Short Papers) Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes
2018	J	`jnl`	Premise selection with neural networks and distributed representation of features. CoRR Andrzej Stanislaw Kucik, Konstantin Korovin
2017	—	`conf`	Towards an Abstraction-Refinement Framework for Reasoning with Large Theories. IWIL@LPAR Julio César López-Hernández, Konstantin Korovin
2016	J	`jnl`	Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA. CoRR Andrew Currin, Konstantin Korovin, Maria Ababi, Katherine Roper, Douglas B. Kell, Philip J. Day, Ross D. King
2016	A	`conf`	Predicate Elimination for Preprocessing in First-Order Theorem Proving. SAT Zurab Khasidashvili, Konstantin Korovin
2015	—	`conf`	EPR-based k-induction with Counterexample Guided Abstraction Refinement. GCAI Zurab Khasidashvili, Konstantin Korovin, Dmitry Tsarkov
2014	—	`conf`	Skolemization Modulo Theories. ICMS Konstantin Korovin, Margus Veanes
2014	B	`conf`	Towards Conflict-Driven Learning for Virtual Substitution. CASC Konstantin Korovin, Marek Kosta, Thomas Sturm
2014	—	`conf`	Towards Conflict-Driven Learning for Virtual Substitution. SMT Konstantin Korovin, Marek Kosta, Thomas Sturm
2014	—	`ed.`	UNIF 2012 Post-Worskhop Proceedings. The 26th International Workshop on Unification, Manchester, UK, July 1, 2012 UNIF Santiago Escobar, Konstantin Korovin, Vladimir V. Rybakov
2013	—	`ed.`	27th International Workshop on Unification, UNIF 2013, Eindhoven, Netherlands, June 26, 2013 UNIF@RTA/TLCA Konstantin Korovin, Barbara Morawska
2013	Misc	`conf`	Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
2013	—	`conf`	From Resolution and DPLL to Solving Arithmetic Constraints. FroCos Konstantin Korovin
2013	—	`ed.`	IWIL 2012: The 9th International Workshop on the Implementation of Logics, Merida, Venezuela, March 10, 2012 IWIL@LPAR Konstantin Korovin, Stephan Schulz, Eugenia Ternovska
2013	—	`conf`	Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning. Programming Logics Konstantin Korovin
2013	—	`conf`	Instantiations, Zippers and EPR Interpolation. LPAR (short papers) Nikolaj S. Bjørner, Arie Gurfinkel, Konstantin Korovin, Ori Lahav
2013	—	`conf`	Non-cyclic Sorts for First-Order Satisfiability. FroCos Konstantin Korovin
2012	A	`conf`	EPR-Based Bounded Model Checking at Word Level. IJCAR Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov
2012	B	`conf`	Preprocessing techniques for first-order clausification. FMCAD Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
2011	—	`conf`	GoRRiLA and Hard Reality. Ershov Memorial Conference Konstantin Korovin, Andrei Voronkov
2011	—	`conf`	Implementing Conflict Resolution. Ershov Memorial Conference Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
2011	A	`conf`	Solving Systems of Linear Inequalities by Bound Propagation. CADE Konstantin Korovin, Andrei Voronkov
2010	B	`conf`	Encoding industrial hardware verification problems into effectively propositional logic. FMCAD Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
2010	—	`conf`	Labelled Unit Superposition Calculi for Instantiation-Based Reasoning. LPAR (Yogyakarta) Konstantin Korovin, Christoph Sticksel
2010	A	`conf`	iProver-Eq: An Instantiation-Based Theorem Prover with Equality. IJCAR Konstantin Korovin, Christoph Sticksel
2009	A	`conf`	Conflict Resolution. CP Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
2009	A	`conf`	Instantiation-Based Automated Reasoning: From Theory to Practice. CADE Konstantin Korovin
2008	A	`conf`	iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description). IJCAR Konstantin Korovin
2007	B	`conf`	Integrating Linear Arithmetic into Superposition Calculus. CSL Konstantin Korovin, Andrei Voronkov
2006	B	`conf`	Theory Instantiation. LPAR Harald Ganzinger, Konstantin Korovin
2005	J	`jnl`	Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. Konstantin Korovin, Andrei Voronkov
2005	B	`conf`	Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS Konstantin Korovin, Andrei Voronkov
2004	B	`conf`	Integrating Equational Reasoning into Instantiation-Based Theorem Proving. CSL Harald Ganzinger, Konstantin Korovin
2003	A	`conf`	An AC-Compatible Knuth-Bendix Order. CADE Konstantin Korovin, Andrei Voronkov
2003	A*	`conf`	New Directions in Instantiation-Based Theorem Proving. LICS Harald Ganzinger, Konstantin Korovin
2003	A*	`conf`	Orienting Equalities with the Knuth-Bendix Order. LICS Konstantin Korovin, Andrei Voronkov
2003	J	`jnl`	Orienting rewrite rules with the Knuth-Bendix order. Inf. Comput. Konstantin Korovin, Andrei Voronkov
2002	J	`jnl`	Knuth-Bendix constraint solving is NP-complete CoRR Konstantin Korovin, Andrei Voronkov
2002	—	`conf`	The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures. FSTTCS Konstantin Korovin, Andrei Voronkov
2001	A*	`conf`	Knuth-Bendix Constraint Solving Is NP-Complete. ICALP Konstantin Korovin, Andrei Voronkov
2001	—	`conf`	Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order. RTA Konstantin Korovin, Andrei Voronkov
2000	A*	`conf`	A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. LICS Konstantin Korovin, Andrei Voronkov
2000	—	`conf`	The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable. ARW Konstantin Korovin, Andrei Voronkov