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

DOI10.1007/978-3-031-37703-7_11zbMATH Open1545.68074MaRDI QIDQ6535536FDOQ6535536

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

Publication date: 12 January 2024

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

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)

Cites Work

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

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)