Portal de Periódicos da CAPES

Capítulo de livro Acesso aberto Produção Nacional Revisado por pares

BIBTEX RIS

Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format

2023; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-031-30823-9_19

1611-3349

Bruno Andreotti, Hanna Lachnitt, Haniel Barbosa,

Formal Methods in Verification

Abstract Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with reconstruction support in the proof assistants Isabelle/HOL and Coq. The format is close to SMT-LIB and allows both coarse- and fine-grained steps, facilitating proof production. However, it lacks a stand-alone checker, which harms its usability and hinders its adoption. Moreover, the coarse-grained steps can be too expensive to check and lead to verification failures. We present Carcara , an independent proof checker and elaborator for Alethe, implemented in Rust. It aims to increase the adoption of the format by providing push-button proof-checking for Alethe proofs, focusing on efficiency and usability; and by providing elaboration for coarse-grained steps into fine-grained ones, increasing the potential success rate of checking Alethe proofs in performance-critical validators, such as proof assistants. We evaluate Carcara over a large set of Alethe proofs generated from SMT-LIB problems and show that it has good performance and its elaboration techniques can make proofs easier to check.