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

[Haniel Barbosa]

Hello,

I would like to participate in the group. 

Best,

Clark Barrett <barrett at cs.stanford.edu> writes:

> 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


-- 
Haniel Barbosa
https://homepages.dcc.ufmg.br/~hbarbosa/