\textsc{CoqCryptoLine}: a verified model checker with certified results

DOI10.1007/978-3-031-37703-7_11MaRDI QIDQ6535536zbMATHFDO

Authors Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

Publication date 12 January 2024

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Certified verification for algebraic abstraction
• Formal certification of code-based cryptographic proofs
• Verified cryptographic code for everybody
• scientific article; zbMATH DE number 1798181

Cites work

• scientific article; zbMATH DE number 1726532 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• scientific article; zbMATH DE number 7378548 (Why is no real title available?)
• An introduction to small scale reflection in Coq
• Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
• CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Uppaal in a nutshell
• Verified model checking of timed automata

Cited in

(1)

• Certified verification for algebraic abstraction

This page was built for publication: \textsc{CoqCryptoLine}: a verified model checker with certified results

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535536)