Numerical MMATh Verified essential algorithms for solving differential equations
| Type of Publication: | Dissertation |
| Publication status: | Published |
| URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-2-wy9t0l1jof5y2 |
| Author: | Hölle, Stefan |
| Year of publication: | 2019 |
| Summary in another language: |
Wie lässt sich mathematisch beweisen, dass numerische Algorithmen korrekt arbeiten? Eine mögliche Antwort auf diese Kernfrage gibt die vorliegende Arbeit. Dazu wird ein mathematisches Modell numerischer Algorithmen vorgestellt.
Durch eine präzise Definition von Darstellungen und Algorithmen können Rechnerobjekte und mathematische Objekte miteinander verbunden werden. Damit wird die Lücke zwischen mathematischer Theorie und Implementierung verringert. Es ist dann möglich, im Sinne von deduktiver Verifikation Aussagen über Algorithmen zu beweisen, die mithilfe der axiomatisch angenommenen Grundalgorithmen aufgebaut werden. Nachdem Darstellungen für endlichen Mengen und Funktionen eingeführt wurden, werden die Möglichkeiten des Modells an verschiedenen Beispielen aus dem Bereich Differentialgleichungen aufgezeigt. Um praktisch relevante Vektorräume zu beschreiben, werden Sammlungen eingeführt. Diese zunächst rekursiv definierte Klasse von Funktionen erlaubt es, vorhandene Strukturen in Anwendungsproblemen in die mathematische Beschreibung zu übernehmen. Als Teil des MMATh Projektes dient das Modell dieser Arbeit auch dazu, den zugehörigen MMATh Interpreter zu testen. Definitionen und Sätze werden entsprechend in einer formalen Sprache formuliert. Beweise werden auf hohem Detailgrad ausgeführt, um notwendige Beweisschritte zu identifizieren. Ein langfristiges Ziel des Projekt ist es, aus formalen mathematischen Texten automatisch verifizierten Code einer beliebigen Programmiersprache zu erzeugen, falls diese Sprache in der Lage ist die axiomatisch geforderten Algorithmen darzustellen. Als erster Schritt wurden hierzu die verifizierten Algorithmen manuell in Scala-Code übersetzt |
| Examination date (for dissertations): | Dec 20, 2019 |
| Dissertation note: | Doctoral dissertation, University of Konstanz |
| Subject (DDC): | 510 Mathematics |
| Keywords: | Deductive Verification, MMATh, Formal Language, Verified Algorithms, Differential Equations |
| Link to License: | In Copyright |
Cite This
Files in this item
![[PDF]](/themes/Kops/images/mimes/pdf.png "PDF file"){kind=small}
![[File]](/themes/Kops/images/mime.png){kind=small}
HÖLLE, Stefan, 2019. Numerical MMATh Verified essential algorithms for solving differential equations [Dissertation]. Konstanz: University of Konstanz
@phdthesis{Holle2019Numer-48245, title={Numerical MMATh Verified essential algorithms for solving differential equations}, year={2019}, author={Hölle, Stefan}, address={Konstanz}, school={Universität Konstanz} }
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/rdf/resource/123456789/48245"> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dcterms:issued>2019</dcterms:issued> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/5/Hoelle_2-wy9t0l1jof5y2.pdf"/> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/6/Hoelle_Langversion_2-wy9t0l1jof5y2.pdf"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/39"/> <dc:rights>terms-of-use</dc:rights> <dc:contributor>Hölle, Stefan</dc:contributor> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:language>eng</dc:language> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:title>Numerical MMATh Verified essential algorithms for solving differential equations</dcterms:title> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/3/Implementation.zip"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/48245"/> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/3/Implementation.zip"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/6/Hoelle_Langversion_2-wy9t0l1jof5y2.pdf"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2020-01-16T14:07:42Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2020-01-16T14:07:42Z</dcterms:available> <dc:creator>Hölle, Stefan</dc:creator> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/48245/5/Hoelle_2-wy9t0l1jof5y2.pdf"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/39"/> </rdf:Description> </rdf:RDF>
Downloads since Jan 16, 2020 (Information about access statistics)
| Hoelle_Langversion_2-wy9t0l1jof5y2.pdf | 12 |
| Hoelle_2-wy9t0l1jof5y2.pdf | 56 |
| Implementation.zip | 4 |
This item appears in the following Collection(s)
Search KOPS
Browse
My Account
