Computer Science Colloquium
Andrei Voronkov
University of Manchester
Solving Systems of Linear Inequalities by Bound Propagation
Wed 09.10.2013, 14:00, 60 minutesScience Park 3, S3 055
Abstract
We introduce a new method for solving systems of linear inequalities over the reals and rationals. The method is called bound propagation and incorporates many state-of-the-art techniques from DPLL-style reasoning, including analogues of unit propagation, inequality/clause learning, variable selection/ordering and backjumping. We implemented bound propagation in the first-order theorem prover Vampire. We describe the method, report experimental results on a number of benchmarks and compare them with those by state-of-the-art SMT solvers.Bio
Andrei Voronkov is Professor of Formal Methods at the University of Manchester. He received his MSc degree in Mathematics from Novosibirsk State University in 1982 and his PhD degree in Algebra and Mathematical Logic in 1987. After that he worked as researcher in the Institute of Mathematics in Novosibirsk in 1987-1991, European Computer Industry Research Centre in Munich in 1991-1992 and Docent in Uppsala University in 1993-1999.He joined the University of Manchester as Professor in 1999. His current interests include automated theorem proving, program analysis, verification, computational logic, Web services and automatic document processing. He has published over 150 technical papers and book chapters on these topics as well as on mathematical logic, linear optimisation, database theory and computation theory. The theorem prover Vampire implemented by him and his students has won 25 world championship titles in theorem proving at the annual competition CASC. He also implemented the conference management system EasyChair with almost 1,000,000 registered users. He has been on editorial boards of several journals, programme chair of more than 20 international conferences, and invited or tutorial speaker at over 60 international conferences and workshops.
Invited by Prof. Dr. Armin Biere, Institut für Formale Modelle und Verifikation
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).