Travelled to:1 × Australia
1 × Greece
1 × Ireland
1 × Poland
1 × Portugal
1 × Russia
1 × Sweden
13 × USA
2 × Austria
2 × Canada
2 × Denmark
2 × Japan
2 × Spain
2 × Switzerland
3 × The Netherlands
4 × Germany
4 × Italy
5 × United Kingdom
Collaborated with:∅ L.Kovács K.Korovin A.Riazanov K.Hoder A.Degtyarev T.Rybina J.A.N.Pérez G.Reger I.Narasamdya E.Dantsin Y.Gurevich L.Maksimova S.G.Vorobyov M.Suda D.Tishkovsky A.Constantin S.Pettifer G.Moser N.Bjørner N.Tillmann L.Bachmair H.Ganzinger Y.Matiyasevich E.Kotelnikov S.Robillard T.A.Henzinger T.Hottelier U.Hustadt B.Konev R.Nieuwenhuis T.Hillenbrand M.S.0001 M.Emmer Z.Khasidashvili C.Sticksel P.Narendran M.Veanes
Talks about:logic (10) order (9) theorem (7) program (7) bendix (6) proof (6) knuth (6) problem (5) vampir (5) system (5)
♂ Person: Andrei Voronkov
DBLP: Voronkov:Andrei
Facilitated 3 volumes:
KN
Ed
EdContributed to:
20152014
201420132013
2013
2012
20122011
20112010
20102009
2009
2009200920082007
2007
20072005200420032003
2003
200320022001200120012000
20002000
20001999
19991998199819981998199719961996
1995
1994199219911990
19902016201820192017Wrote 65 papers:
- CADE-2015-RegerSV #game studies
- Playing with AVATAR (GR, MS, AV), pp. 399–415.
- CADE-2015-RegerTV #proving
- Cooperating Proof Attempts (GR, DT, AV), pp. 339–355.
- ASE-2014-Voronkov
- Keynote talk: EasyChair (AV), pp. 3–4.
- CAV-2014-Voronkov #architecture #first-order #named #proving #theorem proving
- AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
- CADE-2013-HoderV
- The 481 Ways to Split a Clause and Deal with Propositional Variables (KH, AV), pp. 450–464.
- CAV-2013-KovacsV #first-order #proving #theorem proving
- First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
- DocEng-2013-ConstantinPV #named
- PDFX: fully-automated PDF-to-XML conversion of scientific literature (AC, SP, AV), pp. 177–180.
- IJCAR-2012-EmmerKKSV #bound #model checking #word
- EPR-Based Bounded Model Checking at Word Level (ME, ZK, KK, CS, AV), pp. 210–224.
- POPL-2012-HoderKV #game studies #proving
- Playing in the grey area of proofs (KH, LK, AV), pp. 259–272.
- CADE-2011-HoderV #reasoning #scalability
- Sine Qua Non for Large Theory Reasoning (KH, AV), pp. 299–314.
- CADE-2011-KorovinV #bound #linear
- Solving Systems of Linear Inequalities by Bound Propagation (KK, AV), pp. 369–383.
- CADE-2011-KovacsMV #on the #order
- On Transfinite Knuth-Bendix Orders (LK, GM, AV), pp. 384–399.
- TACAS-2011-HoderKV #generative #invariant
- Invariant Generation in Vampire (KH, LK, AV), pp. 60–64.
- IJCAR-2010-HoderKV
- Interpolation and Symbol Elimination in Vampire (KH, LK, AV), pp. 188–195.
- VMCAI-2010-HenzingerHKV #invariant #matrix #type inference
- Invariant and Type Inference for Matrices (TAH, TH, LK, AV), pp. 163–179.
- CADE-2009-KovacsV
- Interpolation and Symbol Elimination (LK, AV), pp. 199–213.
- FASE-2009-KovacsV #array #invariant #proving #source code #theorem proving #using
- Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.
- SAS-2009-VoronkovN
- Inter-program Properties (AV, IN), pp. 343–359.
- TACAS-2009-BjornerTV #analysis #source code #string
- Path Feasibility Analysis for String-Manipulating Programs (NB, NT, AV), pp. 307–321.
- IJCAR-2008-PerezV #effectiveness #logic #proving
- Proof Systems for Effectively Propositional Logic (JANP, AV), pp. 426–440.
- CADE-2007-PerezV #bound #effectiveness #encoding #logic #ltl #model checking
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic (JANP, AV), pp. 346–361.
- CSL-2007-KorovinV #calculus #linear
- Integrating Linear Arithmetic into Superposition Calculus (KK, AV), pp. 223–237.
- SAT-2007-PerezV #effectiveness #encoding #logic #problem
- Encodings of Problems in Effectively Propositional Logic (JANP, AV), p. 3.
- SAS-2005-NarasamdyaV
- Finding Basic Block and Variable Correspondence (IN, AV), pp. 251–267.
- IJCAR-2004-HustadtKRV #named #proving
- TeMP: A Temporal Monodic Prover (UH, BK, AR, AV), pp. 326–330.
- IJCAR-2004-RiazanovV #constraints #performance
- Efficient Checking of Term Ordering Constraints (AR, AV), pp. 60–74.
- CADE-2003-KorovinV #order
- An AC-Compatible Knuth-Bendix Order (KK, AV), pp. 47–59.
- CADE-2003-RiazanovV #performance #relational #retrieval #standard
- Efficient Instance Retrieval with Standard and Relational Path Indexing (AR, AV), pp. 380–396.
- CSL-2003-MaksimovaV #calculus #complexity #problem
- Complexity of Some Problems in Modal and Intuitionistic Calculi (LM, AV), pp. 397–412.
- CSL-2003-RybinaV #infinity #model checking #performance
- Fast Infinite-State Model Checking in Integer-Based Systems (TR, AV), pp. 546–573.
- ICALP-2003-RybinaV #bound #formal method
- Upper Bounds for a Theory of Queues (TR, AV), pp. 714–724.
- LICS-2003-KorovinV #order
- Orienting Equalities with the Knuth-Bendix Order (KK, AV), p. 75–?.
- CAV-2002-RybinaV #canonical #infinity #model checking #using
- Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking (TR, AV), pp. 386–400.
- ICALP-2001-KorovinV #constraints #theorem proving
- Knuth-Bendix Constraint Solving Is NP-Complete (KK, AV), pp. 979–992.
- IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving
- On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
- IJCAR-2001-RiazanovV
- Vampire 1.1 (AR, AV), pp. 376–380.
- IJCAR-2001-Voronkov #algorithm #automation #deduction #performance
- Algorithms, Datastructures, and other Issues in Efficient Automated Deduction (AV), pp. 13–28.
- RTA-2001-KorovinV #order #using #verification
- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order (KK, AV), pp. 137–153.
- CADE-2000-DegtyarevV
- Stratified Resolution (AD, AV), pp. 365–384.
- KR-2000-Voronkov #using
- Deciding K using inverse-K (AV), pp. 198–209.
- LICS-2000-KorovinV #algebra
- A Decision Procedure for the Existential Theory of Term Algebras with the Knuth-Bendix Ordering (KK, AV), pp. 291–302.
- LICS-2000-RybinaV #algebra
- A Decision Procedure for Term Algebras with Queues (TR, AV), pp. 279–290.
- LICS-2000-Voronkov #calculus #how #logic #proving
- How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi (AV), pp. 401–412.
- PODS-2000-DantsinV #complexity #query
- Expressive Power and Data Complexity of Query Languages for Trees and Lists (ED, AV), pp. 157–165.
- CADE-1999-RiazanovV
- Vampire (AR, AV), pp. 292–296.
- CADE-1999-Voronkov #named #proving #theorem proving
- KK: a theorem prover for K (AV), pp. 383–387.
- FoSSaCS-1999-DantsinV #algorithm #nondeterminism #polynomial #set #unification
- A Nondeterministic Polynomial-Time Unification Algorithm for Bags, Sets and Trees (ED, AV), pp. 180–196.
- CADE-1998-BachmairGV #constraints #similarity
- Elimination of Equality via Transformation with Ordering Constraints (LB, HG, AV), pp. 175–190.
- LICS-1998-Voronkov #automation #reasoning #semantics #theorem
- Herbrand’s Theorem, Automated Reasoning and Semantics Tableaux (AV), pp. 252–263.
- PODS-1998-VorobyovV #complexity #logic programming #recursion #source code
- Complexity of Nonrecursive Logic Programs with Complex Values (SGV, AV), pp. 244–253.
- RTA-1998-DegtyarevGNVV #decidability
- The Decidability of Simultaneous Rigid E-Unification with One Variable (AD, YG, PN, MV, AV), pp. 181–195.
- ICALP-1997-GurevichV #monad #problem
- Monadic Simultaneous Rigid E-Unification and Related Problems (YG, AV), pp. 154–165.
- CADE-1996-Voronkov #logic #similarity
- Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (AV), pp. 32–46.
- LICS-1996-DegtyarevMV #algorithm #problem
- Simultaneous E-Unification and Related Algorithmic Problems (AD, YM, AV), pp. 494–502.
- LICS-1996-DegtyarevV #decidability #logic #problem
- Decidability Problems for the Prenex Fragment of Intuitionistic Logic (AD, AV), pp. 503–512.
- ICLP-1995-DegtyarevV #horn clause #similarity
- A New Procedural Interpretation of Horn Clauses with Equality (AD, AV), pp. 565–579.
- PLILP-1994-Voronkov #bottom-up #implementation
- An Implementation Technique for a Class of Bottom-Up Procedures (AV), pp. 147–164.
- CADE-1992-Voronkov #logic #proving #standard #theorem proving
- Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
- CSL-1991-Voronkov #on the #synthesis
- On Completeness of Program Synthesis Systems (AV), pp. 411–418.
- CADE-1990-Voronkov #logic #named
- LISS — The Logic Inference Search System (AV), pp. 677–678.
- ESOP-1990-Voronkov #formal method #logic #programming #towards
- Towards the Theory of Programming in Constructive Logic (AV), pp. 421–435.
- IJCAR-2016-HoderR0V
- Selecting the Selection (KH, GR, MS0, AV), pp. 313–329.
- IJCAR-2018-KotelnikovKV #encoding #imperative #source code
- A FOOLish Encoding of the Next State Relations of Imperative Programs (EK, LK, AV), pp. 405–421.
- CADE-2019-RegerV #induction #proving
- Induction in Saturation-Based Proof Search (GR, AV), pp. 477–494.
- POPL-2017-KovacsRV #quantifier #reasoning
- Coming to terms with quantified reasoning (LK, SR, AV), pp. 260–270.