Andrei Voronkov

Publication Activity (10 Years)

Years Active: 1987-2024
Publications (10 Years): 37

Top Venues

CoRR

CADE

GCAI

CICM

Publications

Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
Program Synthesis in Saturation. CoRR (2024)
Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
Reducibility Constraints in Superposition. IJCAR (1) (2024)
Petra Hozzová, Daneshvar Amrollahi, Márton Hajdú, Laura Kovács, Andrei Voronkov, Eva Maria Wagner
Synthesis of Recursive Programs in Saturation. IJCAR (1) (2024)
Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
Getting Saturated with Induction. CoRR (2024)
Laura Kovács, Petra Hozzová, Márton Hajdú, Andrei Voronkov
Induction in Saturation. IJCAR (1) (2024)
Petra Hozzová, Laura Kovács, Chase Norman, Andrei Voronkov
Program Synthesis in Saturation. CADE (2023)
Konstantin Korovin, Laura Kovács, Giles Reger, Johannes Schoisswohl, Andrei Voronkov
ALASCA: Reasoning in Quantified Linear Arithmetic. TACAS (1) (2023)
Márton Hajdú, Petra Hozzová, Laura Kovács, Giles Reger, Andrei Voronkov
Getting Saturated with Induction. Principles of Systems Design (2022)
Márton Hajdú, Laura Kovács, Michael Rawson, Andrei Voronkov
The Vampire Approach to Induction (short paper). PAAR@IJCAR (2022)
Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
Inductive Benchmarks for Automated Reasoning. CICM (2021)
Petra Hozzová, Laura Kovács, Andrei Voronkov
Integer Induction in Saturation. CADE (2021)
Giles Reger, Johannes Schoisswohl, Andrei Voronkov
Making Theory Reasoning Simpler. TACAS (2) (2021)
Márton Hajdú, Petra Hozzová, Laura Kovács, Andrei Voronkov
Induction with Recursive Definitions in Superposition. FMCAD (2021)
Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov
Induction with Generalization in Superposition Reasoning. CICM (2020)
Giles Reger, Andrei Voronkov
Induction in Saturation-Based Proof Search. CADE (2019)
Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
A FOOLish Encoding of the Next State Relations of Imperative Programs. IJCAR (2018)
Giles Reger, Martin Suda, Andrei Voronkov
Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. TACAS (1) (2018)
Andrei Voronkov
Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning. SYNASC (2018)
Giles Reger, Martin Suda, Andrei Voronkov
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version). CoRR (2017)
Laura Kovács, Simon Robillard, Andrei Voronkov
Coming to terms with quantified reasoning. POPL (2017)
Laura Kovács, Andrei Voronkov
First-Order Interpolation and Interpolating Proof Systems. LPAR (2017)
Giles Reger, Martin Suda, Andrei Voronkov
Instantiation and Pretending to be an SMT Solver with Vampire. SMT (2017)
Giles Reger, Martin Suda, Andrei Voronkov
Testing a Saturation-Based Theorem Prover: Experiences and Challenges. TAP@STAF (2017)
Giles Reger, Martin Suda, Andrei Voronkov
New Techniques in Clausal Form Generation. GCAI (2016)
Giles Reger, Martin Suda, Andrei Voronkov, Krystof Hoder
Selecting the Selection. CoRR (2016)
Giles Reger, Nikolaj Bjørner, Martin Suda, Andrei Voronkov
AVATAR Modulo Theories. GCAI (2016)
Giles Reger, Martin Suda, Andrei Voronkov
Finding Finite Models in Multi-sorted First-Order Logic. SAT (2016)
Giles Reger, Martin Suda, Andrei Voronkov
Finding Finite Models in Multi-Sorted First Order Logic. CoRR (2016)
Laura Kovács, Simon Robillard, Andrei Voronkov
Coming to Terms with Quantified Reasoning. CoRR (2016)
Evgenii Kotelnikov, Laura Kovács, Martin Suda, Andrei Voronkov
A Clausal Normal Form Translation for FOOL. GCAI (2016)
Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov
Selecting the Selection. IJCAR (2016)
Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
The vampire and the FOOL. CPP (2016)
Evgenii Kotelnikov, Laura Kovács, Giles Reger, Andrei Voronkov
The Vampire and the FOOL. CoRR (2015)
Giles Reger, Dmitry Tishkovsky, Andrei Voronkov
Cooperating Proof Attempts. CADE (2015)
Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CICM (2015)
Giles Reger, Martin Suda, Andrei Voronkov
Playing with AVATAR. CADE (2015)
Evgenii Kotelnikov, Laura Kovács, Andrei Voronkov
A First Class Boolean Sort in First-Order Theorem Proving and TPTP. CoRR (2015)
Andrei Voronkov
AVATAR: The Architecture for First-Order Theorem Provers. CAV (2014)
Ashutosh Gupta, Laura Kovács, Bernhard Kragl, Andrei Voronkov
Extensional Crisis and Proving Identity. ATVA (2014)
Andrei Voronkov
Keynote talk: EasyChair. ASE (2014)
Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
Experimenting with SAT Solvers in Vampire. MICAI (1) (2014)
Giles Reger, Martin Suda, Andrei Voronkov
The Challenges of Evaluating a New Feature in Vampire. Vampire Workshop (2014)
Armin Biere, Ioan Dragan, Laura Kovács, Andrei Voronkov
SAT solving experiments in Vampire. Vampire Workshop (2014)
Alexandru Constantin, Steve Pettifer, Andrei Voronkov
PDFX: fully-automated PDF-to-XML conversion of scientific literature. ACM Symposium on Document Engineering (2013)
Laura Kovács, Andrei Mantsivoda, Andrei Voronkov
The Inverse Method for Many-Valued Logics. MICAI (1) (2013)
Ioan Dragan, Konstantin Korovin, Laura Kovács, Andrei Voronkov
Bound Propagation for Arithmetic Reasoning in Vampire. SYNASC (2013)
Laura Kovács, Andrei Voronkov
First-Order Theorem Proving and Vampire. CAV (2013)
Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics (2013)
Juan Antonio Navarro Pérez, Andrei Voronkov
Planning with Effectively Propositional Logic. Programming Logics (2013)
Krystof Hoder, Andrei Voronkov
The 481 Ways to Split a Clause and Deal with Propositional Variables. CADE (2013)
Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
Translating regular expression matching into transducers. J. Appl. Log. 10 (1) (2012)
Krystof Hoder, Andreas Holzer, Laura Kovács, Andrei Voronkov
Vinter: A Vampire-Based Tool for Interpolation. APLAS (2012)
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)
Krystof Hoder, Laura Kovács, Andrei Voronkov
Playing in the grey area of proofs. POPL (2012)
Konstantin Korovin, Andrei Voronkov
GoRRiLA and Hard Reality. Ershov Memorial Conference (2011)
Laura Kovács, Georg Moser, Andrei Voronkov
On Transfinite Knuth-Bendix Orders. CADE (2011)
Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
Implementing Conflict Resolution. Ershov Memorial Conference (2011)
Krystof Hoder, Andrei Voronkov
Sine Qua Non for Large Theory Reasoning. CADE (2011)
Konstantin Korovin, Andrei Voronkov
Solving Systems of Linear Inequalities by Bound Propagation. CADE (2011)
Krystof Hoder, Laura Kovács, Andrei Voronkov
Invariant Generation in Vampire. TACAS (2011)
Krystof Hoder, Laura Kovács, Andrei Voronkov
Case Studies on Invariant Generation Using a Saturation Theorem Prover. MICAI (1) (2011)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1 (7) (2011)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware (2010)
Josef Urban, Krystof Hoder, Andrei Voronkov
Evaluation of Automated Theorem Proving on the Mizar Mathematical Library. ICMS (2010)
Andrei Voronkov
EasyChair. WWV (2010)
Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov
Encoding industrial hardware verification problems into effectively propositional logic. FMCAD (2010)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware (2010)
Thomas A. Henzinger, Thibaud Hottelier, Laura Kovács, Andrei Voronkov
Invariant and Type Inference for Matrices. VMCAI (2010)
Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
Translating Regular Expression Matching into Transducers. SYNASC (2010)
Krystof Hoder, Laura Kovács, Andrei Voronkov
Interpolation and Symbol Elimination in Vampire. IJCAR (2010)
Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov
Conflict Resolution. CP (2009)
Krystof Hoder, Andrei Voronkov
Comparing Unification Algorithms in First-Order Theorem Proving. KI (2009)
Andrei Voronkov, Iman Narasamdya
Inter-program Properties. SAS (2009)
Nikolaj Bjørner, Nikolai Tillmann, Andrei Voronkov
Path Feasibility Analysis for String-Manipulating Programs. TACAS (2009)
Laura Kovács, Andrei Voronkov
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. SYNASC (2009)
Andrei Voronkov
Satisfiability and Theories. SYNASC (2009)
Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov
Verifying equivalence of memories using a first order logic theorem prover. FMCAD (2009)
Laura Kovács, Andrei Voronkov
Interpolation and Symbol Elimination. CADE (2009)
Laura Kovács, Andrei Voronkov
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. FASE (2009)
Juan Antonio Navarro Pérez, Andrei Voronkov
Proof Systems for Effectively Propositional Logic. IJCAR (2008)
Juan Antonio Navarro Pérez, Andrei Voronkov
Encodings of Problems in Effectively Propositional Logic. SAT (2007)
Juan Antonio Navarro Pérez, Andrei Voronkov
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. CADE (2007)
Konstantin Korovin, Andrei Voronkov
Integrating Linear Arithmetic into Superposition Calculus. CSL (2007)
Andrei Voronkov
Inconsistencies in Ontologies. JELIA (2006)
Mohammed K. Jaber, Andrei Voronkov
Implementation of UNIDOOR, a Deductive Object-Oriented Database System. ADBIS (2006)
Ian Horrocks, Andrei Voronkov
Reasoning Support for Expressive Ontology Languages Using a Theorem Prover. FoIKS (2006)
Mohammed K. Jaber, Andrei Voronkov
UNIDOOR: a Deductive Object-Oriented Database Management System. ICDE (2006)
Dimitri Chubarov, Andrei Voronkov
Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. MFCS (2005)
Dimitri Chubarov, Andrei Voronkov
Solving First-Order Constraints over the Monadic Class. Mechanizing Mathematical Reasoning (2005)
Konstantin Korovin, Andrei Voronkov
Random Databases and Threshold for Monotone Non-recursive Datalog. MFCS (2005)
Juan Antonio Navarro Pérez, Andrei Voronkov
Generation of Hard Non-Clausal Random Satisfiability Problems. AAAI (2005)
Iman Narasamdya, Andrei Voronkov
Finding Basic Block and Variable Correspondence. SAS (2005)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
05431 Executive Summary - Deduction and Applications. Deduction and Applications (2005)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
05431 Abstracts Collection - Deduction and Applications. Deduction and Applications (2005)
Konstantin Korovin, Andrei Voronkov
Knuth-Bendix constraint solving is NP-complete. ACM Trans. Comput. Log. 6 (2) (2005)
Alexandre Riazanov, Andrei Voronkov
Efficient instance retrieval with standard and relational path indexing. Inf. Comput. 199 (1-2) (2005)
Alexandre Riazanov, Andrei Voronkov
Efficient Checking of Term Ordering Constraints. IJCAR (2004)
Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov
TeMP: A Temporal Monodic Prover. IJCAR (2004)
Alexandre Riazanov, Andrei Voronkov
Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36 (1-2) (2003)

Andrei Voronkov.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Andrei Voronkov