Privacy-preserving Automated Reasoning

Explore privacy-preserving automated reasoning in this keynote address from the Conference on Computer-Aided Verification (CAV'23). Delve into the concept of privacy-preserving formal reasoning, addressing the gap in current formal method techniques that do not consider privacy requirements. Examine the development of a privacy-preserving Boolean satisfiability (ppSAT) solver, which enables mutually distrustful parties to evaluate the conjunction of their input formulas while maintaining privacy. Learn about the oblivious variant of the classic DPLL algorithm and its integration with secure two-party computation techniques. Discover a zero-knowledge protocol for proving the unsatisfiability of Boolean formulas in propositional logic, based on resolution proof of unsatisfiability and utilizing polynomial equivalence checking. Gain insights into future directions for privacy-preserving SMT solvers and fully automated privacy-preserving program verification in this comprehensive 1-hour and 16-minute presentation by Ruzica Piskac from Yale University.