Partial correctness of GCD algorithm

DOI10.2478/FORMA-2018-0014MaRDI QIDQ2311524zbMATH OpenOpenAlexWikidataFDO

Authors Ievgen Ivanov, Artur Korniłowicz, M. S. Nikitchenko

Publication date 10 July 2019

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported

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

zbMATH Keywords

greatest common divisornominative dataprogram verification

Mathematics Subject Classification ID

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

Recommendations

• Partial correctness of a power algorithm
• Partial correctness of a factorial algorithm
• A Greatest Common Divisor Algorithm
• scientific article; zbMATH DE number 910705
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials

Cites work

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

Cited in

(6)

• Partial correctness of a Fibonacci algorithm
• Partial correctness of a factorial algorithm
• Partial correctness of a power algorithm
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• General theory and tools for proving algorithms in nominative data systems
• Partial correctness of an algorithm computing Lucas sequences

Describes a project that uses

Uses Software

• Mizar

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

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