Proof producing synthesis of arithmetic and cryptographic hardware
From MaRDI portal
Recommendations
- Computer-aided cryptographic proofs
- Hardware-Dependent Proofs of Numerical Programs
- scientific article; zbMATH DE number 7378548
- Cryptography arithmetic. Algorithms and hardware architectures
- Hardware Private Circuits: From Trivial Composition to Full Verification
- Algorithmic problems in the symbolic approach to the verification of automatically synthesized cryptosystems
- Computer-Aided Security Proofs for the Working Cryptographer
- Practical homomorphic message authenticators for arithmetic circuits
Cites work
- A Brief Overview of HOL4
- An approach to the specification and verification of a hardware compilation scheme
- Functional Correctness Proofs of Encryption Algorithms
- Handshake Circuits
- Higher Order Logic and Hardware Verification
- scientific article; zbMATH DE number 1614686 (Why is no real title available?)
- scientific article; zbMATH DE number 50156 (Why is no real title available?)
- scientific article; zbMATH DE number 1455096 (Why is no real title available?)
Cited in
(10)- Adapting functional programs to higher order logic
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- Proof-producing translation of higher-order logic into pure and stateful ML
- Hardware-Dependent Proofs of Numerical Programs
- Coquet: a Coq library for verifying hardware
- A Brief Overview of HOL4
- Formal verification for high-assurance behavioral synthesis
- Mechanised wire-wise verification of Handel-C synthesis
- An approach to the specification and verification of a hardware compilation scheme
- Modeling a hardware synthesis methodology in Isabelle
This page was built for publication: Proof producing synthesis of arithmetic and cryptographic hardware
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2642982)
