Konstantin Korovin

CoRR, 2024

ESBMC v7.4: Harnessing the Power of Intervals - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023

The ksmt calculus is a <i>δ</i>-complete decision procedure for non-linear constraints.

[BibT_eX]

[DOI]

Margarita V. Korovina

Norbert Th. Müller

Theor. Comput. Sci., October, 2023

ESBMC v7.4: Harnessing the Power of Intervals.

[BibT_eX]

[DOI]

CoRR, 2023

Graph Sequence Learning for Premise Selection.

[BibT_eX]

[DOI]

Edvard K. Holden

CoRR, 2023

ALASCA: Reasoning in Quantified Linear Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2023

Guiding an Instantiation Prover with Graph Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Refining Unification with Abstraction.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

LGEM<sup>+</sup>: A First-Order Logic Framework for Automated Improvement of Metabolic Network Models Through Abduction.

[BibT_eX]

[DOI]

Proceedings of the Discovery Science - 26th International Conference, 2023

2022

Machine Learning Meets The Herbrand Universe.

[BibT_eX]

[DOI]

CoRR, 2022

Position Paper: Towards a Hybrid Approach to Protect Against Memory Safety Vulnerabilities.

[BibT_eX]

[DOI]

Proceedings of the IEEE Secure Development Conference, 2022

ESBMC-CHERI: towards verification of C programs for CHERI platforms with ESBMC.

[BibT_eX]

[DOI]

Proceedings of the ISSTA '22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18, 2022

Combining Constraint Solving and Bayesian Techniques for System Optimization.

[BibT_eX]

[DOI]

Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, 2022

Ground Joinability and Connectedness in the Superposition Calculus.

[BibT_eX]

[DOI]

André Duarte

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2021

Bayesian Optimisation with Formal Guarantees.

[BibT_eX]

[DOI]

CoRR, 2021

AC Simplifications and Closure Redundancies in the Superposition Calculus.

[BibT_eX]

[DOI]

André Duarte

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2021

Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving.

[BibT_eX]

[DOI]

Edvard K. Holden

Proceedings of the Intelligent Computer Mathematics - 14th International Conference, 2021

Optimization of Fan-Beam Radiation Pattern of Cylindrical Phased Array.

[BibT_eX]

[DOI]

Proceedings of the 13th International Congress on Ultra Modern Telecommunications and Control Systems and Workshops, 2021

The ksmt Calculus Is a δ-complete Decision Procedure for Non-linear Constraints.

[BibT_eX]

[DOI]

Margarita V. Korovina

Norbert Th. Müller

Proceedings of the Automated Deduction - CADE 28, 2021

2020

Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation.

[BibT_eX]

[DOI]

Proceedings of the 2020 Formal Methods in Computer Aided Design, 2020

Implementing Superposition in iProver (System Description).

[BibT_eX]

[DOI]

André Duarte

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

A CDCL-Style Calculus for Solving Non-linear Constraints.

[BibT_eX]

[DOI]

Margarita V. Korovina

Norbert Th. Müller

Proceedings of the Frontiers of Combining Systems - 12th International Symposium, 2019

2018

Premise selection with neural networks and distributed representation of features.

[BibT_eX]

[DOI]

Andrzej Stanislaw Kucik

Julio César López-Hernández

CoRR, 2018

An Abstraction-Refinement Framework for Reasoning with Large Theories.

[BibT_eX]

[DOI]

Julio César López-Hernández

Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017

Towards an Abstraction-Refinement Framework for Reasoning with Large Theories.

[BibT_eX]

[DOI]

Proceedings of the IWIL@LPAR 2017 Workshop and LPAR-21 Short Presentations, 2017

2016

Computing exponentially faster: Implementing a nondeterministic universal Turing machine using DNA.

[BibT_eX]

[DOI]

CoRR, 2016

Predicate Elimination for Preprocessing in First-Order Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2016, 2016

2015

EPR-based k-induction with Counterexample Guided Abstraction Refinement.

[BibT_eX]

[DOI]

Dmitry Tsarkov

Proceedings of the Global Conference on Artificial Intelligence, 2015

2014

Skolemization Modulo Theories.

[BibT_eX]

[DOI]

Margus Veanes

Proceedings of the Mathematical Software - ICMS 2014, 2014

Towards Conflict-Driven Learning for Virtual Substitution.

[BibT_eX]

[DOI]

Marek Kosta

Thomas Sturm

Proceedings of the Computer Algebra in Scientific Computing - 16th International Workshop, 2014

2013

Bound Propagation for Arithmetic Reasoning in Vampire.

[BibT_eX]

[DOI]

Proceedings of the 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2013

Instantiations, Zippers and EPR Interpolation.

[BibT_eX]

[DOI]

Proceedings of the LPAR 2013, 2013

From Resolution and DPLL to Solving Arithmetic Constraints.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

Non-cyclic Sorts for First-Order Satisfiability.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2013

Inst-Gen - A Modular Approach to Instantiation-Based Automated Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

Preprocessing techniques for first-order clausification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 2012

EPR-Based Bounded Model Checking at Word Level.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

GoRRiLA and Hard Reality.

[BibT_eX]

[DOI]

Proceedings of the Perspectives of Systems Informatics, 2011

Implementing Conflict Resolution.

[BibT_eX]

[DOI]

Nestan Tsiskaridze

Proceedings of the Perspectives of Systems Informatics, 2011

Solving Systems of Linear Inequalities by Bound Propagation.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Labelled Unit Superposition Calculi for Instantiation-Based Reasoning.

[BibT_eX]

[DOI]

Christoph Sticksel

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Encoding industrial hardware verification problems into effectively propositional logic.

[BibT_eX]

[DOI]

Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

iProver-Eq: An Instantiation-Based Theorem Prover with Equality.

[BibT_eX]

[DOI]

Christoph Sticksel

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

Conflict Resolution.

[BibT_eX]

[DOI]

Nestan Tsiskaridze

Proceedings of the Principles and Practice of Constraint Programming, 2009

Instantiation-Based Automated Reasoning: From Theory to Practice.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2009

2008

iProver - An Instantiation-Based Theorem Prover for First-Order Logic (System Description).

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

2007

Integrating Linear Arithmetic into Superposition Calculus.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2006

Theory Instantiation.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the Logic for Programming, 2006

2005

Knuth-Bendix constraint solving is NP-complete.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2005

Random Databases and Threshold for Monotone Non-recursive Datalog.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Foundations of Computer Science 2005, 2005

2004

Integrating Equational Reasoning into Instantiation-Based Theorem Proving.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the Computer Science Logic, 18th International Workshop, 2004

2003

Orienting rewrite rules with the Knuth-Bendix order.

[BibT_eX]

[DOI]

Inf. Comput., 2003

Orienting Equalities with the Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

New Directions in Instantiation-Based Theorem Proving.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 2003

An AC-Compatible Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

The Decidability of the First-Order Theory of the Knuth-Bendix Order in the Case of Unary Signatures.

[BibT_eX]

[DOI]

Proceedings of the FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, 2002

2001

Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

2000

A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

The Existential Theories of Term Algebras with the Knuth-Bendix Orderings are Decidable.

[BibT_eX]

[DOI]