Georg Gottlob, University of Oxford and TU Wien
Hypergraph Transversals, Monotone Boolean Formula Dualization, and SAT (Slide)
Abstract: Hypergraph Transversals have been studied in Mathematics for a long time. Generating minimal transversals of a hypergraph is equivalent to monotone Boolean DNF dualization, which, in turn, is equivalent to restricted versions of SAT. These important problems have many applications in Computer Science, for instance, in data mining. The complexity of checking whether two hypergraphs are dual to each other has been open for about 40 years. I will give an overview of various applications and equivalent formulations, and of some algorithms and complexity bounds for this mysterious problem.
Georg Gottlob is a Royal Society Research Professor and a Professor of Informatics at Oxford University. and at TU Wien. At Oxford he is a Fellow of St John’s College. His interests include knowledge representation, logic and complexity, and database and Web querying. He has received various awards, among which the Wittgenstein Award (Austria) and the Ada Lovelace Medal (UK). He is a Fellow of the Royal Society, of the Austrian and German National Academies of Science, and of the Academia Europaea. He was a founder of Lixto, a company specialised in semi-automatic web logic-based data extraction which was acquired by McKinsey in 2013. Gottlob was awarded an ERC Advanced Investigator’s Grant for the project “DIADEM: Domain-centric Intelligent Automated Data Extraction Methodology”. Based on the results of this project, he co-founded Wrapidity Ltd, a company that specialised in fully automated web data extraction, which was acquired in 2016 by Meltwater.
Personal Webpage: https://www.cs.ox.ac.uk/people/georg.gottlob/ – https://www.dbai.tuwien.ac.at/staff/gottlob/
Aarti Gupta, Princeton University, US
With a little help from structured friends (Slide: Part 1 – Part 2)
Abstract: SAT and SMT solvers have enabled tremendous advances in automated verification and synthesis in a wide range of application domains. However, to extract maximum mileage, it is often helpful to suitably formulate the verification problem or supplement the solvers with other techniques to bridge the gap between satisfiability on one hand and verification/synthesis on the other. In this talk, I will describe some techniques that leverage the structure of the underlying models to further enhance the capabilities of SAT/SMT-based verification. I will show successful instances from the domains of computer networks, hardware designs, and theorem-proving.
Aarti Gupta is a Professor in the Department of Computer Science at Princeton University. She received a PhD in Computer Science from Carnegie Mellon University. Her research is in the areas of formal verification of programs and systems, automatic decision procedures, and electronic design automation. She has served on the technical program committees of many leading conferences, and is currently serving on the Steering Committee of the CAV (Computer Aided Verification) Conference. She is an ACM Fellow.
Personal Webpage: http://www.cs.princeton.edu/~aartig