[Proof Complexity] MIAO seminar Tue Mar 18 at 14:00 CET with Haniel Barbosa: SMT proof production, checking and reconstruction

[Jakob Nordström]

Dear all,

On Tuesday March 18 at 14:00 CET we will have the opportunity to listen 
to the MIAO seminar "SMT proof production, checking and reconstruction" 
given by Haniel Barbosa from Universidade Federal de Minas Gerais. You 
find the abstract at the bottom of this message.

This will be a video seminar at https://lu-se.zoom.us/j/61925271827 . 
Please feel free to share this information with colleagues who you think 
might be interested. We are also hoping to record the seminar and post 
on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch 
for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular 
talk, and then after a break a ca-1-hour in-depth technical presentation 
with (hopefully) a lot of interaction. The intention is that the first 
part of the seminar will give all listeners a self-contained overview of 
some exciting research results, and after the break people who have the 
time and interest will get an opportunity to really get into the 
technical details. (However, for those who feel that the first part was 
enough, it is perfectly fine to just discretely drop out during the 
break. No questions asked; no excuses needed.)

More information about the MIAO seminar series can be found at 
https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive 
these announcements, or receive several copies of them, please send a 
message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Tuesday Mar 18 at 14:00 on Zoom
*SMT proof production, checking and reconstruction
*(Haniel Barbosa, Universidade Federal de Minas Gerais)
/
Satisfiability modulo theories (SMT) solvers can be hard to trust, since 
it generally means assuming their large and complex codebases do not 
contain bugs leading to wrong results. Machine-checkable certificates, 
via proofs of the logical reasoning the solver has performed, address 
this issue by decoupling confidence in the results from the solver's 
implementation. In this talk we will describe the extensive proof 
infrastructure of the state-of-the-art SMT solver cvc5, which has 
enabled the production of proofs in a number of complex domains. We will 
also show how these proofs are checked or reconstructed in different 
formats by different systems, from ad-hoc high-performance proof 
checkers to proof assistants such as Lean.

*/Speaker bio: /*Haniel Barbosa is a tenured assistant professor in the 
Department of Computer Science at Universidade Federal de Minas Gerais 
(UFMG), in Belo Horizonte, Brazil. He fell in love with automated 
reasoning and its applications during his PhD at Inria Nancy, under the 
direction of Prof. Pascal Fontaine, and subsequently as a postdoctoral 
researcher at the University of Iowa. His research focuses on improving 
satisfiability modulo theories (SMT) solvers for formal verification and 
on making them more trustworthy via the production and checking of proof 
certificates. He is also a senior technical lead for the 
state-of-the-art SMT solver cvc5.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se