The aim of this WG is to promote the output of detailed, checkable proofs from automated theorem provers. Work is under way for FOL/HOL theorem provers and SMT solvers, but the expressivity of their input languages renders the task significantly more complicated than e.g., in the propositional SAT world, with a higher need of coordination.

Activities

  • August 2022: WG2 meeting co-located with the PAAR workshop and a workshop dedicated to sharing libraries of formal proofs during FLOC at Haifa (Israel)

  • Summer 2022: next edition of VTSA at Saarbr├╝cken (Germany) with a focus on proof-generating verification systems