Partial correctness of GCD algorithm

DOI10.2478/FORMA-2018-0014zbMath1422.11240OpenAlexW2907818187WikidataQ128663203 ScholiaQ128663203MaRDI QIDQ2311524

Ievgen Ivanov, Artur Korniłowicz, Mykola Nikitchenko

Publication date: 10 July 2019

Published in: Formalized Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2478/forma-2018-0014

zbMATH Keywords

greatest common divisorprogram verificationnominative data

Mathematics Subject Classification ID

Number-theoretic algorithms; complexity (11Y16) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Primality (11Y11)

Related Items (2)

Partial correctness of a power algorithm ⋮ Partial correctness of a Fibonacci algorithm

Uses Software

• Mizar

Cites Work

• Four decades of {\textsc{Mizar}}. Foreword
• Proving properties of programs on hierarchical nominative data
• Implementation of the composition-nominative approach to program formalization in Mizar
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Simple-named complex-valued nominative data -- definition and basic operations
• Kleene algebra of partial predicates

This page was built for publication: Partial correctness of GCD algorithm