\textsc{CoqCryptoLine}: a verified model checker with certified results
From MaRDI portal
Publication:6535536
DOI10.1007/978-3-031-37703-7_11zbMATH Open1545.68074MaRDI QIDQ6535536
Ming-Hsien Tsai, Bo-Yin Yang, Bow-Yaw Wang, Jiaxiang Liu, Xiaomu Shi, Yu-Fu Fu
Publication date: 12 January 2024
Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Uppaal in a nutshell
- Verified model checking of timed automata
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
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)
