BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Ruzica Piskac (Yale): Privacy-preserving Automated Reasoning
DTSTART:20230904T140000
DTEND:20230904T150000
DTSTAMP:20260916T032119Z
UID:0ab1f06dda096ef3173130242896c693c35c5bbebca2111f7a6361a7
CATEGORIES:Conferences - Seminars
DESCRIPTION:Formal methods offer a vast collection of techniques to analyz
 e and ensure the correctness\, robustness\, and safety of software and har
 dware systems against a specification. The efficacy of such tools allows t
 heir application to even large-scale industrial codebases.  Despite the s
 ignificant success of formal method techniques\, privacy requirements are 
 not considered in their design. When using automated reasoning tools\, the
  implicit requirement is that the formula to be proved is public. To overc
 ome this problem\, we propose the concept of privacy-preserving formal rea
 soning.\nWe first present privacy-preserving Boolean satisfiability (ppSAT
 ) solver\, which allows mutually distrustful parties to evaluate the conju
 nction of their input formulas while maintaining privacy. We construct an 
 oblivious variant of the classic DPLL algorithm which can be integrated wi
 th existing secure two-party computation (2PC) techniques. This solver tak
 es input two private SAT formulas and checks if their conjunction is satis
 fiable. However\, in verification\, the users might want to keep their pro
 grams private and show in a privacy-preserving manner that their programs 
 adhere to the given public specification.  To this end\, we developed a z
 ero-knowledge protocol for proving the unsatisfiability of Boolean formula
 s in propositional logic. Our protocol is based on a resolution proof of u
 nsatisfiability. We encoded verification of the resolution proof using pol
 ynomial equivalence checking\, which enabled us to use fast ZKP protocols 
 for polynomial satisfiability.\nFinally\, we will conclude the talk by out
 lining future directions towards privacy-preserving SMT solvers and fully 
 automated privacy-preserving program verification.\n\nBio : Ruzica Piskac 
 is an associate professor of computer science at Yale University. Her rese
 arch interests span the areas of programming languages\, software verifica
 tion\, automated reasoning\, and code synthesis. A common thread in Ruzica
 ’s research is improving software reliability and trustworthiness using 
 formal techniques. Ruzica joined Yale in 2013 as an assistant professor an
 d prior to that\, she was an independent research group leader at the Max 
 Planck Institute for Software Systems in Germany. In July 2019\, she was n
 amed the Donna L. Dubinsky Associate Professor of Computer Science\, one o
 f the highest recognition that an untenured faculty member at Yale can rec
 eive. Ruzica has received various recognitions for research and teaching\,
  including the Patrick Denantes Prize for her PhD thesis\, a CACM Research
  Highlight paper\, an NSF CAREER award\, the Facebook Communications and N
 etworking award\, the Microsoft Research Award for the Software Engineerin
 g Innovation Foundation (SEIF)\, the Amazon Research Award\, and the 2019 
 Ackerman Award for Teaching and Mentoring.
LOCATION:BC 129 https://plan.epfl.ch/?room==BC%20129
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR