Andrei Voronkov

{{For|other people called Andrei Voronkov|Andrei Voronkov (disambiguation)}}

{{Infobox scientist

| name = Andrei Voronkov

| birth_name = Andrei Anatolievič Voronkov

| native_name = Андрей Анатольевич Воронков

| native_name_lang = ru

| image = Andrei Voronkov - Turing 100 - 2012 - Portrait.jpg

| image_size =

| alt =

| caption = Andrei Voronkov at the Alan Turing Centenary Conference, June 24th, 2012

| birth_date = {{Birth date and age|1959|05|14}}{{LCAuth|n92045267|Andrei Voronkov||}}{{cite web |author=Anon |year=2016 |archive-url=https://web.archive.org/web/20160809103025/https://beta.companieshouse.gov.uk/officers/KMmptYHYk0T1HVo8Es81NQjzd88/appointments |archive-date=2016-08-09 |url=https://beta.companieshouse.gov.uk/officers/KMmptYHYk0T1HVo8Es81NQjzd88/appointments |url-status=live |website=companieshouse.gov.uk |publisher=Companies House |location=London |title=Andrei VORONKOV Date of birth May 1959}}

| birth_place =

| death_date =

| death_place =

| resting_place =

| resting_place_coordinates =

| residence =

| citizenship =

| nationality =

| fields = Formal methods

| workplaces = {{Plainlist|

  • University of Manchester
  • Novosibirsk State University{{Cite book | last1 = Voronkov | first1 = A. A. | author-link = Andrei Voronkov| chapter = Deductive program synthesis and Markov's principle | doi = 10.1007/3-540-18740-5_105 | title = Fundamentals of Computation Theory | series = Lecture Notes in Computer Science | volume = 278 | pages = 479–482 | year = 1987 | isbn = 978-3-540-18740-0 }}}}

| alma_mater = Novosibirsk State University

| thesis_title = Realizability and Program Synthesis

| thesis_url =

| thesis_year = 1987

| doctoral_advisor =

| academic_advisors =

| doctoral_students =

| notable_students =

| known_for ={{Plainlist|

| influences =

| influenced =

| awards = {{Plainlist|

| signature =

| signature_alt =

| website = {{Plainlist|

  • {{URL|voronkov.com}}
  • {{URL|manchester.ac.uk/research/andrei.voronkov}}}}}}Andrei Anatolievič Voronkov (born 1959) is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.{{cite web |url=http://www.manchester.ac.uk/research/Andrei.voronkov/ |title=Prof Andrei Voronkov, research profile - personal details (The University of Manchester) |access-date=2012-06-08}}{{Cite journal | doi = 10.1145/502807.502810| title = Complexity and expressive power of logic programming| journal = ACM Computing Surveys| volume = 33| issue = 3| pages = 374| year = 2001| last1 = Dantsin | first1 = E. | last2 = Eiter | first2 = T. | last3 = Gottlob | first3 = G. | author-link3 = Georg Gottlob| last4 = Voronkov | first4 = A. | s2cid = 518049| author-link4 = Andrei Voronkov}}{{Cite book | doi = 10.1145/2494266.2494271| chapter = PDFX: fully-automated PDF-to-XML conversion of scientific literature| title = Proceedings of the 2013 ACM symposium on Document engineering - Doc Eng '13| pages = 177| year = 2013| last1 = Constantin | first1 = A. | last2 = Pettifer | first2 = S. | author-link2 = Steve Pettifer| last3 = Voronkov | first3 = A.| author-link3 = Andrei Voronkov | isbn = 9781450317894| s2cid = 17173414| url = https://pure.manchester.ac.uk/ws/files/33527522/FULL_TEXT.PDF| chapter-url = https://www.escholar.manchester.ac.uk/uk-ac-man-scw:218911}}

Education

Voronkov was educated at Novosibirsk State University, graduating with a PhD in 1987.{{cite thesis |degree=PhD |first=Andrei|last=Voronkov |title=Realizability and Program Synthesis |publisher=Novosibirsk State University |date=1987 |author-link=Andrei Voronkov}}{{cite web|archive-url=https://web.archive.org/web/20160304030237/http://www.cs.man.ac.uk/~voronkov/all_publications.html|archive-date=2016-03-04|url=http://www.cs.man.ac.uk/~voronkov/all_publications.html|title=Papers by Andrei Voronkov|publisher=University of Manchester|website=cs.man.ac.uk|first=Andrei|last=Voronkov|year=2016}}

Research

Voronkov is known for the Vampire{{cite conference |last1=Kotelnikov |first1=Evgenii |book-title=Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs - CPP 2016 |last2=Kovács |first2=Laura |last3=Reger |first3=Giles |last4=Voronkov |first4=Andrei |year=2016 |pages=37–48 |doi=10.1145/2854065.2854071 |title=The vampire and the FOOL |isbn=9781450341271|arxiv=1510.04821 }} automated theorem prover, the EasyChair conference management software, the Handbook of Automated Reasoning (with John Alan Robinson, 2001),{{cite book |title=Handbook of Automated Reasoning |editor-last=Robinson |editor-first=John Alan |editor-last2=Voronkov |editor-first2=Andrei | publisher=MIT Press + Elsevier | year=2001 |isbn=9780444508133}}{{cite book |last1=Sekar |first1=R. |title=Handbook of Automated Reasoning |last2=Ramakrishnan |first2=I.V. |last3=Voronkov |first3=Andrei |editor-last=Robinson |editor-first=John Alan |editor-last2=Voronkov |editor-first2=Andrei |year=2001 |pages=1853–1964 |chapter=Term Indexing |doi=10.1016/B978-044450813-3/50028-X |isbn=9780444508133}}{{cite book |last1=Degtyarev |first1=Anatoli |title=Handbook of Automated Reasoning |last2=Voronkov |first2=Andrei |editor-last=Robinson |editor-first=John Alan |editor-last2=Voronkov |editor-first2=Andrei |year=2001 |pages=611–706 |doi=10.1016/B978-044450813-3/50012-6 |chapter=Equality Reasoning in Sequent-Based Calculi |hdl=11858/00-001M-0000-0014-7A79-8 |isbn=9780444508133}}{{cite book |last1=Degtyarev |first1=Anatoli |title=Handbook of Automated Reasoning |last2=Voronkov |first2=Andrei |editor-last=Robinson |editor-first=John Alan |editor-last2=Voronkov |editor-first2=Andrei |year=2001 |pages=179–272 |doi=10.1016/B978-044450813-3/50006-0 |chapter=The Inverse Method |isbn=9780444508133}} and as organiser of the Alan Turing Centenary Conference 2012.{{AcademicSearch|439151}}{{Google Scholar id}}{{DBLP|name=Andrei Voronkov}}{{Scopus}}{{ACMPortal}}

Voronkov's research has been funded by the Engineering and Physical Sciences Research Council (EPSRC).{{cite web|archive-url=https://web.archive.org/web/20150512062225/http://gow.epsrc.ac.uk/NGBOViewPerson.aspx?PersonId=27394|archive-date=2015-05-12|url=http://gow.epsrc.ac.uk/NGBOViewPerson.aspx?PersonId=27394|title=Grants awarded to Andrei Voronkov by the EPSRC|author=Anon|year=2015|publisher=Engineering and Physical Sciences Research Council|location=Swindon|website=epsrc.ac.uk}}{{cite web|archive-url=https://web.archive.org/web/20160809094533/http://gtr.rcuk.ac.uk/person/871947ED-289A-43DB-BB3A-DB6955907ED5|archive-date=2016-08-09|url=http://gtr.rcuk.ac.uk/person/871947ED-289A-43DB-BB3A-DB6955907ED5|title=UK Government grants awarded to Andrei Voronkov|publisher=Research Councils UK|website=rcuk.ac.uk|location=Swindon|author=Anon|year=2016}}

Awards and honours

In 2015, his contributions to the field of automated reasoning were recognized with the Herbrand Award.{{cite web |title=Herbrand Award |url=http://cadeinc.org/Herbrand-Award |publisher=CADE inc. |website=cadeinc.org}} He has won 25 division titles in the CADE ATP System Competition (CASC) at the Conference on Automated Deduction (CADE) since 1999.{{citation needed|date=August 2016}}

References