Proving an execution of an algorithm correct?

DOI10.1007/978-3-031-42753-4_17MaRDI QIDQ6118838zbMATH OpenFDO

Authors James H. Davenport

Publication date 28 February 2024

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-031-42753-4_17

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Recommendations

• scientific article; zbMATH DE number 524110
• A computer checked algebraic verification of a distributed summation algorithm
• scientific article; zbMATH DE number 1389645
• scientific article; zbMATH DE number 1745035
• Recent advances in program verification through computer algebra

Cites work

• A formal quantifier elimination for algebraically closed fields
• A new decision method for elementary algebra
• Algebraic Properties of the Elementary Functions of Analysis
• Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
• Factoring Polynomials Over Large Finite Fields
• Factoring polynomials with rational coefficients
• Factorization in Z[x]
• Factors of iterated resultants and discriminants
• Fast recognition of alternating and symmetric Galois groups
• scientific article; zbMATH DE number 3497890 (Why is no real title available?)
• scientific article; zbMATH DE number 3556250 (Why is no real title available?)
• scientific article; zbMATH DE number 1273670 (Why is no real title available?)
• scientific article; zbMATH DE number 1047740 (Why is no real title available?)
• scientific article; zbMATH DE number 3415973 (Why is no real title available?)
• scientific article; zbMATH DE number 3048552 (Why is no real title available?)
• scientific article; zbMATH DE number 3056446 (Why is no real title available?)
• Improving the use of equational constraints in cylindrical algebraic decomposition
• Integration of elementary functions
• Intégration algorithmique des fonctions élémentairement transcendantes sur une courbe algébrique
• Multivariate Polynomial Factorization
• On Hensel factorization. I
• On propagation of equational constraints in CAD-based quantifier elimination
• On the integration of algebraic functions
• Real quantifier elimination is doubly exponential
• Some undecidable problems involving elementary functions of a real variable
• Studies in Equisingularity II. Equisingularity in Codimension 1 (and Characteristic Zero)
• The Problem of Integration in Finite Terms
• The Risch Differential Equation Problem
• Thom's lemma, the coding of real algebraic numbers and the computation of the topology of semi-algebraic sets
• Validity proof of Lazard's method for CAD construction

This page was built for publication: Proving an execution of an algorithm correct?

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