Andrei Voronkov

Andrei Voronkov
Andrei Voronkov at the Alan Turing Centenary Conference, June 24th, 2012
Born	Andrei A. Voronkov 1959 (age 56–57)[1]
Fields	Formal methods
Institutions	University of Manchester Novosibirsk State University[2]
Alma mater	Novosibirsk State University[2]
Thesis	Realizability and Program Synthesis (1987)
Doctoral students	Dmitri Chubarov[3] Shasha Feng Kryštof Hoder[4][5] Mohammed Khazal Jaber[6] Konstantin Korovin[7][8] Iman Narasamdya[9] Juan Antonio Navarro Pérez[10] Alexandre Riazanov[11] Andrei Tchaltsev Lars Thalmann[12] Nestan Tsiskaridze[13][14] Margus Veanes[15][16]
Known for	Vampire theorem prover[17] EasyChair
Notable awards	25 division titles in CASC since 1999
Website www.voronkov.com www.manchester.ac.uk/research/andrei.voronkov

Andrei A. Voronkov is a Professor of Formal methods in the School of Computer Science at the University of Manchester.^[18][19][20]

Education

Voronkov was educated at Novosibirsk State University,^[2] graduating with a PhD in 1987.^[21][22]

Research

Voronkov is known for the Vampire^[17] automated theorem prover, the EasyChair conference management software, the Handbook of Automated Reasoning (with John Alan Robinson, 2001),^[23] and as organiser of the Alan Turing Centenary Conference 2012.^{[24][25][26][27][28]}

Voronkov's research has been funded by the Engineering and Physical Sciences Research Council.^[29]

In 2015, his contributions to the field of automated reasoning were recognised with the Herbrand Award.^[30]

References

1. "Voronkov, Andrej". Viaf. Retrieved 11 August 2014.
2. Voronkov, A. A. (1987). "Deductive program synthesis and Markov's principle". Fundamentals of Computation Theory. Lecture Notes in Computer Science 278. pp. 479–482. doi:10.1007/3-540-18740-5_105. ISBN 978-3-540-18740-0.
3. Chubarov, D.; Voronkov, A. (2005). "Solving First-Order Constraints over the Monadic Class". Mechanizing Mathematical Reasoning. Lecture Notes in Computer Science 2605. p. 132. doi:10.1007/978-3-540-32254-2_8. ISBN 978-3-540-25051-7.
4. Hoder, Kryštof (2012). Practical aspects of automated first-order reasoning (PhD thesis). University of Manchester.
5. Hoder, K. T.; Voronkov, A. (2009). "Comparing Unification Algorithms in First-Order Theorem Proving". KI 2009: Advances in Artificial Intelligence. Lecture Notes in Computer Science 5803. p. 435. doi:10.1007/978-3-642-04617-9_55. ISBN 978-3-642-04616-2.
6. Jaber, M. K.; Voronkov, A. (2006). "Implementation of UNIDOOR, a Deductive Object-Oriented Database System". Advances in Databases and Information Systems. Lecture Notes in Computer Science 4152. p. 155. doi:10.1007/11827252_14. ISBN 978-3-540-37899-0.
7. Korovin, Konstantin (2003). Knuth-Bendix Orders in Automated Deduction and Term Rewriting (PhD thesis). University of Manchester.
8. Korovin, K.; Voronkov, A. (2000). "A decision procedure for the existential theory of term algebras with the Knuth-Bendix ordering". Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332). p. 291. doi:10.1109/LICS.2000.855777. ISBN 0-7695-0725-5.
9. Voronkov, A.; Narasamdya, I. (2009). "Inter-program Properties". Static Analysis. Lecture Notes in Computer Science 5673. p. 343. doi:10.1007/978-3-642-03237-0_23. ISBN 978-3-642-03236-3.
10. Navarro, J. A.; Voronkov, A. (2008). "Proof Systems for Effectively Propositional Logic". Automated Reasoning. Lecture Notes in Computer Science 5195. p. 426. doi:10.1007/978-3-540-71070-7_36. ISBN 978-3-540-71069-1.
11. Riazanov, A.; Voronkov, A. (1999). "Vampire". Automated Deduction — CADE-16. Lecture Notes in Computer Science 1632. p. 292. doi:10.1007/3-540-48660-7_26. ISBN 978-3-540-66222-8.
12. Fitting, M.; Thalmann, L.; Voronkov, A. (2000). "Term-Modal Logics". Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science 1847. p. 220. doi:10.1007/10722086_19. ISBN 978-3-540-67697-3.
13. Tsiskaridze, Nestan (2011). Conflick Resolution (PhD thesis). University of Manchester.
14. Korovin, K.; Tsiskaridze, N.; Voronkov, A. (2012). "Implementing Conflict Resolution". Perspectives of Systems Informatics. Lecture Notes in Computer Science 7162. p. 362. doi:10.1007/978-3-642-29709-0_31. ISBN 978-3-642-29708-3.
15. Degtyarev, A.; Gurevich, Y.; Narendran, P.; Veanes, M.; Voronkov, A. (2000). "Decidability and complexity of simultaneous rigid -unification with one variable and related results". Theoretical Computer Science 243: 167. doi:10.1016/S0304-3975(98)00185-6.
16. http://voronkov.com/students.cgi
17. Voronkov, A. (1995). "The anatomy of vampire". Journal of Automated Reasoning 15 (2): 237–265. doi:10.1007/BF00881918.
18. "Prof Andrei Voronkov, research profile - personal details (The University of Manchester)". Retrieved 2012-06-08.
19. Dantsin, E.; Eiter, T.; Gottlob, G.; Voronkov, A. (2001). "Complexity and expressive power of logic programming". ACM Computing Surveys 33 (3): 374. doi:10.1145/502807.502810.
20. Constantin, A.; Pettifer, S.; Voronkov, A. (2013). "PDFX: fully-automated PDF-to-XML conversion of scientific literature". Proceedings of the 2013 ACM symposium on Document engineering - Doc Eng '13. p. 177. doi:10.1145/2494266.2494271. ISBN 9781450317894.
21. Voronkov, Andrei (1987). Realizability and Program Synthesis (PhD thesis). Novosibirsk State University.
22. http://www.cs.man.ac.uk/~voronkov/all_publications.html Papers by Andrei Voronkov
23. John Alan Robinson and Andrei Voronkov, ed. (2001). Handbook of Automated Reasoning. MIT Press + Elsevier.
24. List of publications from Microsoft Academic Search
25. http://scholar.google.com/scholar?q=andrei+voronkov Andrei Voronkov publications in Google Scholar
26. Andrei Voronkov's publications indexed by the DBLP Bibliography Server at the University of Trier
27. Andrei Voronkov's publications indexed by the Scopus bibliographic database, a service provided by Elsevier.
28. Andrei Voronkov from the Association for Computing Machinery (ACM) Digital Library
29. http://gow.epsrc.ac.uk/NGBOViewPerson.aspx?PersonId=27394 Grants awarded to Andrei Voronkov by the Engineering and Physical Sciences Research Council
30. "The Herbrand Award for Distinguished Contributions to Automated Reasoning". CADE inc. Retrieved 4 August 2015.