CS Talk: Albert Rubio

Speaker: Albert Rubio

Date: Friday, June 10, 2022

Time: 12 pm - 1:30 pm

Location: HFH 1132

Title: Formal Methods for ZK Proving Systems: Challenges in the Circom Programming Language

Host: Yu Feng.

Abstract:
The most widely studied language in the context of Zero-Knowledge (ZK) proofs is arithmetic circuit satisfiability. In this talk we present circom, a programming language and a compiler that allows the programmer to provide a low-level description of the arithmetic circuit together with an effective way to execute it. Challenging constraint manipulation and analysis problems will be introduced as well as some safety properties of circom programs that need to be checked. We will conclude the talk discussing some new features that will be added to the compiler in the near future.

Bio:
Albert Rubio has been a professor at the Complutense University of Madrid since 2019. Previously, he was a professor at the Technical University of Catalonia since 2008 and got his PhD in Computer Science in 1994. He is the author of more than 70 papers published in the most prestigious conferences and journals, including LICS, CAV or the Journal of ACM. He is the coauthor of a chapter of the Handbook of Automated Reasoning. He started his research working on automated theorem proving and (higher-order) rewriting. Since then, he has worked on the development and application of SMT solvers, as well as on program analysis and verification of programs including SDN networks. He is currently applying formal methods to blockchain technologies and leading the development of the circom language compiler.

This event is sponsored by UCSB PLSE lab and Veridise Inc. Refreshments will be served during the talk.

All are welcome!