Остановите войну!
for scientists:
default search action
Konstantin Korovin
- > Home > Persons > Konstantin Korovin
Publications
- 2024
- [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 - [i11]Franz Brauße, Zurab Khasidashvili, Konstantin Korovin:
SMLP: Symbolic Machine Learning Prover. CoRR abs/2402.01415 (2024) - 2023
- [j3]Franz Brauße, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller:
The ksmt calculus is a δ-complete decision procedure for non-linear constraints. Theor. Comput. Sci. 975: 114125 (2023) - [c49]Ahmed Bhayat, Konstantin Korovin, Laura Kovács, Johannes Schoisswohl:
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, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov:
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) 2023: 647-665 - [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
- [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, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, Lucas C. Cordeiro:
ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC. ISSTA 2022: 773-776 - [c43]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: 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, Konstantin Korovin, Margarita V. Korovina, Norbert Th. Müller:
The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints. CADE 2021: 113-130 - [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) - 2020
- [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] - 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
- [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] - 2016
- [c33]Zurab Khasidashvili, Konstantin Korovin:
Predicate Elimination for Preprocessing in First-Order Theorem Proving. SAT 2016: 361-372 - 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 - 2013
- [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, Konstantin Korovin, Laura Kovács, Andrei Voronkov:
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] - 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 - 2009
- [c14]Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov:
Conflict Resolution. CP 2009: 509-523 - 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
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-04-21 17:41 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint