Dsc

Sheng, Aeacus

doi:10.4230/artifacts.26768

Artifact

Dsc Software

Author Aeacus Sheng

Part of: Collection: Supplementary Materials
License: MIT License
Publication Date: 2026-07-16

Document Identifiers

DOI: 10.4230/artifacts.26768
URN: urn:nbn:de:0030-drops-267684

Author Details

Aeacus Sheng

University of Edinburgh

Content

Software (Source Code): https://github.com/Aeacu2/Dsc
archived version

Version/Status

Content created at: 2026-02-18
Status: Active (at the time of publication 2026-07-16)

Cite As Get BibTex

Aeacus Sheng. Dsc (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/artifacts.26768

Description

Isabelle/HOL verification of real root isolation algorithms based on Descartes' Rule of Signs. Includes a classical bisection algorithm and a Newton-accelerated version.

Subject Classification

Keywords

Computer Algebra
Real Root Isolation
Formal Verification
Isabelle/HOL

Programming Languages

Isabelle
Standard ML

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata

0

Downloads

Any Issues?

Feedback on the Current Page

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail