On Saturday, March 18, 2017, The University of Liège will honoring its recent PhD’s and presenting the insignia of Doctor Honoris Causa to personalities proposed by the Faculties. The Faculty of Applied Sciences will be honoring
Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, and the Southeastern Universities Research Association's Distinguished Scientist Award.
He is the author and co-author of over 500 papers, as well as two books: Reasoning about Knowledge and Finite Model Theory and Its Applications. He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He is the Editor-in-Chief of the Communications of the ACM.
On the occasion of his visit to Liège, Professor M. VARDI will give two lectures in English :
For the past 40 years computer scientists generally believed that NP-complete problems are intractable. In particular, Boolean satisfiability (SAT), as a paradigmatic automated-reasoning problem, has been considered to be intractable. Over the past 20 years, however, there has been a quiet, but dramatic, revolution, and very large SAT instances are now being solved routinely as part of software and hardware design. In this talk I will review this amazing development and show how automated reasoning is now an industrial reality.
I will then describe how we can leverage SAT solving to accomplish other automated-reasoning tasks. Counting the number of satisfying truth assignments of a given Boolean formula or sampling such assignments uniformly at random are fundamental computational problems in computer science with applications in software testing, software synthesis, machine learning, personalized learning, and more. While the theory of these problems has been thoroughly investigated since the 1980s, approximation algorithms developed by theoreticians do not scale up to industrial-sized instances. Algorithms used by the industry offer better scalability, but give up certain correctness guarantees to achieve scalability. We describe a novel approach, based on universal hashing and Satisfiability Modulo Theory, that scales to formulas with hundreds of thousands of variables without giving up correctness guarantees.
This lecture is intended for a general computer science audience and will take place on Friday, March 17, at 11 am, Local R7 of the Institut Montefiore (B28 - Access and Plans)
Automation, driven by technological progress, has been increasing inexorably for the past several decades. Two schools of economic thinking have for many years been engaged in a debate about the potential effects of automation on jobs: will new technology spawn mass unemployment, as the robots take jobs away from humans? Or will the jobs robots take over create demand for new human jobs?
I will present data that demonstrate that the concerns about automation are valid. In fact, technology has been hurting working Americans for the past 40 years. The discussion about humans, machines and work tends to be a discussion about some undetermined point in the far future. But it is time to face reality. The future is now.
This lecture is intended for a general audience and will take place on Friday, 17 March, at 5 pm, Amphitheatres of Europe, Room 204 (B4 - Access and Plans)