[SMT-COMP] [External] [smt-lib] New working group on SMT proofs

[Cesare Tinelli]

Dear member of the SMT community,

Thanks to all who have expressed their interest in joining a working 
group on SMT proofs. A mailing list was created a few months ago for the 
group:

smt-proofs at googlegroups.com

While the the mailing list has been dormant for a while, there has been 
a flurry of activities on proof production and checking in several SMT 
groups, and a number of conversations have been started among members of 
these groups.

In an effort to move these conversations to the list and push the goals 
of the working group, **Haniel Barbosa** has kindly agreed to lead the 
working group.

He will follow up soon with some initial proposals on how to move 
forward.

Best,

Cesare,
also for Clark and Pascal


PS: If you are not in the working group yet and would like to join it, 
please send an email to Haniel (hbarbosa at dcc.ufmg.br) and he will add 
you to the mailing list.





On 5 Aug 2021, at 17:04, Clark Barrett wrote:

> Dear SMT community,
>
> As you know, producing independently checkable proofs has long been a
> stretch goal for SMT solvers, with different solvers offering 
> different
> levels of support for such proofs and largely using independent 
> formats.
> Recently, there has been an increase in interest in this topic, both 
> from
> industry (e.g., Amazon's automated reasoning group) as well as from 
> our own
> community (e.g., the email thread started by Jochen Hoenicke following 
> the
> SMT competition).
>
> As we have done in the past when various SMT topics have garnered
> significant interest, we would like to propose creating a working 
> group on
> SMT proofs.  The purpose of the group is to make sure that many
> perspectives are heard and considered and to develop a roadmap, within 
> the
> context of the overall SMT-LIB standard, that can hopefully synthesize 
> a
> variety of both short-term and long-term goals.
>
> Please reply to this email if you would like to join the working 
> group.  We
> will aim to set up an initial discussion soon.
>
> Best,
>
> Clark Barrett, Pascal Fontaine, and Cesare Tinelli
>
> -- 
> You received this message because you are subscribed to the Google 
> Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to smt-lib+unsubscribe at googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com.