Verification of the Miller-Rabin probabilistic primality test.

DOI10.1016/S1567-8326(02)00065-6MaRDI QIDQ1400288zbMATH OpenFDO

Authors Joe Hurd

Publication date 13 August 2003

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

Formal verificationPrimality testRandom algorithms

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Mechanisation of the AKS algorithm
• The error probability of the Miller-Rabin primality test
• A new probabilistic primality test
• Publication:4293690
• Probabilistic guarded commands mechanized in HOL

Cites work

• scientific article; zbMATH DE number 1670733 (Why is no real title available?)
• scientific article; zbMATH DE number 3882509 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 3569835 (Why is no real title available?)
• scientific article; zbMATH DE number 3597592 (Why is no real title available?)
• scientific article; zbMATH DE number 1178976 (Why is no real title available?)
• scientific article; zbMATH DE number 1927425 (Why is no real title available?)
• scientific article; zbMATH DE number 1863390 (Why is no real title available?)
• A Fast Monte-Carlo Test for Primality
• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• Factoring Polynomials Over Large Finite Fields
• Formal and efficient primality proofs by use of computer algebra oracles
• Proof Checking the RSA Public Key Encryption Algorithm

Cited in

(10)

• Proofs of randomized algorithms in Coq
• A low complexity probabilistic test for integer multiplication
• Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• Mechanisation of the AKS algorithm
• Proof-producing translation of higher-order logic into pure and stateful ML
• The Miller–Rabin test with randomized exponents
• Multidimensional scaling and visualization of patterns in prime numbers
• Computational logic: its origins and applications
• Classification of finite fields with applications

Describes a project that uses

Uses Software

• PVS
• HOL
• NQTHM

This page was built for publication: Verification of the Miller-Rabin probabilistic primality test.

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