报告题目：CDSAT: Conflict-Driven Satisfiability modulo theories and assignments

报 告 人：Maria Paola Bonacina  Professor

主 持 人：张民 副教授

报告时间：2018年5月2日（周三）13:30-14:30

报告地点：中北校区理科大楼B1102报告厅

报告人简介：

Maria Paola Bonacina is Professor of Computer Science at the University degli Studi di Verona. Prior to this she was first Assistant Professor and then Associate Professor of Computer Science at the University of Iowa, where she received NSF RIA and CAREER awards and a Dean Scholar Award. Her research area is automated reasoning, including theorem proving, model building, decision procedures for satisfiability, reasoning for analysis, verification, synthesis of systems, strategy analysis, and distributed deduction.

She gave over one hundred and twenty talks, authored over seventy peer-reviewed papers, and edited two books. Maria Paola was Visiting Research Scholar at the Isaac Newton Institute for Mathematical Sciences of the University of Cambridge, the Computer Science Laboratory of SRI International, where she spent a sabbatical year, and Microsoft Research Redmond. She was Visiting Professor at the University of Manchester and the Technische University Dresden. Maria Paola serves regularly on the Program Committee of CADE (Conference on Automated Deduction), IJCAR (International Joint Conference on Automated Reasoning), and other conferences.

She was Program Chair of CADE-24 in 2013. She was elected thrice to the Board of Trustees of CADE Inc., and twice President of the Board. Maria Paola did postdoc work at INRIA Lorraine and at the Argonne National Laboratory; received a PhD from the State University of New York at Stony Brook, and a Doctorate and a Laurea from the Universita' degli Studi di Milano.

报告摘要：

Many applications require to check the satisfiability of formulae involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory (SMT). This talk presents CDSAT, a new method for Satisfiability Modulo Assignment (SMA),a generalization of SMT where also assignments to variables maybe in the input. Search-based procedures assign values to variables to build a model, and perform conflict-driven inferences to solve conflicts between assignments and formulae. CDSAT extends this paradigm to theory combination, combining for the first time both conflict-driven and black-box theory modules. The conflict-driven reasoning happens in the union of the theories, not only in propositional logic. As there is no hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. CDSAT is sound, complete, terminating, and proof-generating.

(CDSAT is joint work with Stephane Graham-Lengrand and Natarajan Shankar)