| 2025 | CADE | Term Ordering Diagrams. | Mrton Hajd, Robin Coutelier, Laura Kovcs, Andrei Voronkov |
| 2025 | CADE | Partial Redundancy in Saturation. | Mrton Hajd, Laura Kovcs, Andrei Voronkov |
| 2025 | CADE | Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories. | Michael Rawson, Andrei Voronkov, Johannes Schoisswohl, Anja Petkovic Komel |
| 2025 | CAV | The Vampire Diary. | Filip Brtek, Ahmed Bhayat, Robin Coutelier, Mrton Hajd, Matthias Hetzenberger, Petra Hozzov, Laura Kovcs, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, Andrei Voronkov |
| 2024 | IJCAR | Reducibility Constraints in Superposition. | Mrton Hajd, Laura Kovcs, Michael Rawson, Andrei Voronkov |
| 2024 | IJCAR | Synthesis of Recursive Programs in Saturation. | Petra Hozzov, Daneshvar Amrollahi, Mrton Hajd, Laura Kovcs, Andrei Voronkov, Eva Maria Wagner |
| 2024 | IJCAR | Induction in Saturation. | Laura Kovcs, Petra Hozzov, Mrton Hajd, Andrei Voronkov |
| 2023 | CADE | Program Synthesis in Saturation. | Petra Hozzov, Laura Kovcs, Chase Norman, Andrei Voronkov |
| 2023 | TACAS | ALASCA: Reasoning in Quantified Linear Arithmetic. | Konstantin Korovin, Laura Kovcs, Giles Reger, Johannes Schoisswohl, Andrei Voronkov |
| 2021 | CADE | Integer Induction in Saturation. | Petra Hozzov, Laura Kovcs, Andrei Voronkov |
| 2021 | FMCAD | Induction with Recursive Definitions in Superposition. | Mrton Hajd, Petra Hozzov, Laura Kovcs, Andrei Voronkov |
| 2021 | TACAS | Making Theory Reasoning Simpler. | Giles Reger, Johannes Schoisswohl, Andrei Voronkov |
| 2019 | CADE | Induction in Saturation-Based Proof Search. | Giles Reger, Andrei Voronkov |
| 2018 | CADE | A FOOLish Encoding of the Next State Relations of Imperative Programs. | Evgenii Kotelnikov, Laura Kovcs, Andrei Voronkov |
| 2018 | SYNASC | Reasoning with Quantifiers and Theories Using Saturation-Based Reasoning. | Andrei Voronkov |
| 2018 | TACAS | Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2017 | LPAR | First-Order Interpolation and Interpolating Proof Systems. | Laura Kovcs, Andrei Voronkov |
| 2017 | POPL | Coming to terms with quantified reasoning. | Laura Kovcs, Simon Robillard, Andrei Voronkov |
| 2017 | TAP | Testing a Saturation-Based Theorem Prover: Experiences and Challenges. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2016 | CADE | Selecting the Selection. | Krystof Hoder, Giles Reger, Martin Suda, Andrei Voronkov |
| 2016 | CPP | The vampire and the FOOL. | Evgenii Kotelnikov, Laura Kovcs, Giles Reger, Andrei Voronkov |
| 2016 | SAT | Finding Finite Models in Multi-sorted First-Order Logic. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2015 | CADE | Playing with AVATAR. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2015 | CADE | Cooperating Proof Attempts. | Giles Reger, Dmitry Tishkovsky, Andrei Voronkov |
| 2014 | ATVA | Extensional Crisis and Proving Identity. | Ashutosh Gupta, Laura Kovcs, Bernhard Kragl, Andrei Voronkov |
| 2014 | CADE | SAT solving experiments in Vampire. | Armin Biere, Ioan Dragan, Laura Kovcs, Andrei Voronkov |
| 2014 | CADE | The Challenges of Evaluating a New Feature in Vampire. | Giles Reger, Martin Suda, Andrei Voronkov |
| 2014 | CAV | AVATAR: The Architecture for First-Order Theorem Provers. | Andrei Voronkov |
| 2013 | CADE | The 481 Ways to Split a Clause and Deal with Propositional Variables. | Krystof Hoder, Andrei Voronkov |
| 2013 | CAV | First-Order Theorem Proving and Vampire. | Laura Kovcs, Andrei Voronkov |
| 2013 | DocEng | PDFX: fully-automated PDF-to-XML conversion of scientific literature. | Alexandru Constantin, Steve Pettifer, Andrei Voronkov |
| 2013 | SYNASC | Bound Propagation for Arithmetic Reasoning in Vampire. | Ioan Dragan, Konstantin Korovin, Laura Kovcs, Andrei Voronkov |
| 2012 | APLAS | Vinter: A Vampire-Based Tool for Interpolation. | Krystof Hoder, Andreas Holzer, Laura Kovcs, Andrei Voronkov |
| 2012 | CADE | EPR-Based Bounded Model Checking at Word Level. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov |
| 2012 | FMCAD | Preprocessing techniques for first-order clausification. | Krystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2012 | POPL | Playing in the grey area of proofs. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2011 | CADE | Sine Qua Non for Large Theory Reasoning. | Krystof Hoder, Andrei Voronkov |
| 2011 | CADE | Solving Systems of Linear Inequalities by Bound Propagation. | Konstantin Korovin, Andrei Voronkov |
| 2011 | CADE | On Transfinite Knuth-Bendix Orders. | Laura Kovcs, Georg Moser, Andrei Voronkov |
| 2011 | TACAS | Invariant Generation in Vampire. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2010 | CADE | Interpolation and Symbol Elimination in Vampire. | Krystof Hoder, Laura Kovcs, Andrei Voronkov |
| 2010 | FMCAD | Encoding industrial hardware verification problems into effectively propositional logic. | Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov |
| 2010 | SYNASC | Translating Regular Expression Matching into Transducers. | Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov |
| 2010 | VMCAI | Invariant and Type Inference for Matrices. | Thomas A. Henzinger, Thibaud Hottelier, Laura Kovcs, Andrei Voronkov |
| 2009 | CADE | Interpolation and Symbol Elimination. | Laura Kovcs, Andrei Voronkov |
| 2009 | CP | Conflict Resolution. | Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov |
| 2009 | FASE | Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. | Laura Kovcs, Andrei Voronkov |
| 2009 | FMCAD | Verifying equivalence of memories using a first order logic theorem prover. | Zurab Khasidashvili, Mahmoud Kinanah, Andrei Voronkov |
| 2009 | KI | Comparing Unification Algorithms in First-Order Theorem Proving. | Krystof Hoder, Andrei Voronkov |
| 2009 | SAS | Inter-program Properties. | Andrei Voronkov, Iman Narasamdya |
| 2009 | SYNASC | Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. | Laura Kovcs, Andrei Voronkov |
| 2009 | SYNASC | Satisfiability and Theories. | Andrei Voronkov |
| 2009 | TACAS | Path Feasibility Analysis for String-Manipulating Programs. | Nikolaj S. Bjrner, Nikolai Tillmann, Andrei Voronkov |
| 2008 | CADE | Proof Systems for Effectively Propositional Logic. | Juan Antonio Navarro Prez, Andrei Voronkov |
| 2007 | CADE | Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. | Juan Antonio Navarro Prez, Andrei Voronkov |
| 2007 | CSL | Integrating Linear Arithmetic into Superposition Calculus. | Konstantin Korovin, Andrei Voronkov |
| 2007 | SAT | Encodings of Problems in Effectively Propositional Logic. | Juan Antonio Navarro Prez, Andrei Voronkov |
| 2006 | ADBIS | Implementation of UNIDOOR, a Deductive Object-Oriented Database System. | Mohammed K. Jaber, Andrei Voronkov |
| 2006 | ICDE | UNIDOOR: a Deductive Object-Oriented Database Management System. | Mohammed K. Jaber, Andrei Voronkov |
| 2006 | JELIA | Inconsistencies in Ontologies. | Andrei Voronkov |
| 2005 | AAAI | Generation of Hard Non-Clausal Random Satisfiability Problems. | Juan Antonio Navarro Prez, Andrei Voronkov |
| 2005 | MFCS | Basis of Solutions for a System of Linear Inequalities in Integers: Computation and Applications. | Dimitri Chubarov, Andrei Voronkov |
| 2005 | MFCS | Random Databases and Threshold for Monotone Non-recursive Datalog. | Konstantin Korovin, Andrei Voronkov |
| 2005 | SAS | Finding Basic Block and Variable Correspondence. | Iman Narasamdya, Andrei Voronkov |
| 2004 | CADE | TeMP: A Temporal Monodic Prover. | Ullrich Hustadt, Boris Konev, Alexandre Riazanov, Andrei Voronkov |
| 2004 | CADE | Efficient Checking of Term Ordering Constraints. | Alexandre Riazanov, Andrei Voronkov |
| 2003 | CADE | An AC-Compatible Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2003 | CADE | Efficient Instance Retrieval with Standard and Relational Path Indexing. | Alexandre Riazanov, Andrei Voronkov |
| 2003 | CSL | Complexity of Some Problems in Modal and Intuitionistic Calculi. | Larisa Maksimova, Andrei Voronkov |
| 2003 | CSL | Fast Infinite-State Model Checking in Integer-Based Systems (Invited Lecture). | Tatiana Rybina, Andrei Voronkov |
| 2003 | ICALP | Upper Bounds for a Theory of Queues. | Tatiana Rybina, Andrei Voronkov |
| 2003 | IJCAI | Automated Reasoning: Past Story and New Trends. | Andrei Voronkov |
| 2003 | LICS | Orienting Equalities with the Knuth-Bendix Order. | Konstantin Korovin, Andrei Voronkov |
| 2002 | CAV | Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking. | Tatiana Rybina, Andrei Voronkov |
| 2001 | CADE | On the Evaluation of Indexing Techniques for Theorem Proving. | Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov |
| 2001 | CADE | Vampire 1.1 (System Description). | Alexandre Riazanov, Andrei Voronkov |
| 2001 | CADE | Algorithms, Datastructures, and other Issues in Efficient Automated Deduction. | Andrei Voronkov |
| 2001 | ICALP | Knuth-Bendix Constraint Solving Is NP-Complete. | Konstantin Korovin, Andrei Voronkov |
| 2001 | IJCAI | Splitting Without Backtracking. | Alexandre Riazanov, Andrei Voronkov |
| 2000 | CADE | Stratified Resolution. | Anatoli Degtyarev, Andrei Voronkov |
| 2000 | JELIA | Partially Adaptive Code Trees. | Alexandre Riazanov, Andrei Voronkov |
| 2000 | KR | Deciding K using inverse-K. | Andrei Voronkov |
| 2000 | LICS | A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering. | Konstantin Korovin, Andrei Voronkov |
| 2000 | LICS | A Decision Procedure for Term Algebras with Queues. | Tatiana Rybina, Andrei Voronkov |
| 2000 | LICS | How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi. | Andrei Voronkov |
| 2000 | PODS | Expressive Power and Data Complexity of Query Languages for Trees and Lists. | Evgeny Dantsin, Andrei Voronkov |
| 2000 | TABLEAUX | Term-Modal Logics. | Melvin Fitting, Lars Thalmann, Andrei Voronkov |
| 1999 | CADE | Vampire. | Alexandre Riazanov, Andrei Voronkov |
| 1999 | CADE | KK: a theorem prover for K. | Andrei Voronkov |
| 1999 | FOSSACS | A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees. | Evgeny Dantsin, Andrei Voronkov |
| 1998 | CADE | Elimination of Equality via Transformation with Ordering Constraints. | Leo Bachmair, Harald Ganzinger, Andrei Voronkov |
| 1998 | LICS | Herbrand's Theorem, Automated Reasoning and Semantics Tableaux. | Andrei Voronkov |
| 1998 | PODS | Complexity of Nonrecursive Logic Programs with Complex Values. | Sergei G. Vorobyov, Andrei Voronkov |
| 1997 | ICALP | Monadic Simultaneous Rigid E-Unification and Related Problems. | Yuri Gurevich, Andrei Voronkov |
| 1997 | IJCAI | Strategies in Rigid-Variable Methods. | Andrei Voronkov |
| 1997 | LFCS | Complexity of Query Answering in Logic Databases with Complex Values. | Evgeny Dantsin, Andrei Voronkov |
| 1996 | CADE | Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification. | Andrei Voronkov |
| 1996 | JELIA | What You Always Wanted to Know About Rigid E-Unification. | Anatoli Degtyarev, Andrei Voronkov |
| 1996 | LICS | Simultaneous E-Unification and Related Algorithmic Problems. | Anatoli Degtyarev, Yuri V. Matiyasevich, Andrei Voronkov |
| 1996 | LICS | Decidability Problems for the Prenex Fragment of Intuitionistic Logic. | Anatoli Degtyarev, Andrei Voronkov |
| 1996 | TABLEAUX | Proof-Search in Intuitionistic Logic Based on Constraint Satisfaction. | Andrei Voronkov |
| 1995 | CSL | Simultaneous Regid E-Unification Is Undecidable. | Anatoli Degtyarev, Andrei Voronkov |
| 1995 | ICLP | A New Procedural Interpretation of Horn Clauses with Equality. | Anatoli Degtyarev, Andrei Voronkov |
| 1995 | IJCAI | Equality Elimination for the Inverse Method and Extension Procedures. | Anatoli Degtyarev, Andrei Voronkov |
| 1992 | CADE | Theorem Proving in Non-Standard Logics Based on the Inverse Method. | Andrei Voronkov |
| 1992 | ICLP | On Computability by Logic Programs. | Andrei Voronkov |
| 1991 | CSL | On Completeness of Program Synthesis Systems. | Andrei Voronkov |
| 1991 | LPAR | Logic Programming with Bounded Quantifiers. | Andrei Voronkov |
| 1990 | CADE | LISS - The Logic Inference Search System. | Andrei Voronkov |
| 1990 | ESOP | Towards the Theory of Programming in Constructive Logic. | Andrei Voronkov |
| 1987 | FCT | Deductive Program Synthesis and Markov's Principle. | Andrei Voronkov |