Fr, 06.10.2017, 13:30
Formal Verification in Imperative Multivalued Programming over Continuous Data Types

Referent: Prof. Dr. Martin Ziegler, KAIST
Raum: S2|15-201

(joint work with Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, and Norbert Preining)

Inspired and guided by the iRRAM C++ library (Müller 2001), we formally specify a programming language for the paradigm of EXACT REAL COMPUTATION: reliably operating on encapsulated CONTINUOUS data types such as (not necessarily algebraic) real numbers --- imperatively and exactly (no rounding errors) with primitives computable in the sense of Recursive Analysis and a necessarily modified multivalued=non-extensional semantics of tests. We then propose a complete logical system over two types, integers and real numbers, for rigorous correctness proofs of such algorithms. We extend the rules of Hoare Logic to support the formal derivation of such proofs, and have them verified in the Coq Proof Assistant. Our approach is exemplified with three simple numerical example problems: integer rounding, solving systems of linear equations, and continuous root finding.


Technische Universität Darmstadt
Fachbereich Mathematik
Arbeitsgruppe Logik

Schloßgartenstraße 7
64289 Darmstadt

Tel.: +49-(0)6151-1622863
Fax: +49-(0)6151-1622840

Raum S2|15-206
Betina Schubotz

Mo. - Fr.  10:00-15:00

« Dezember 2017 »
Mo Di Mi Do Fr Sa So
48 1 2 3
49 4 5 6 7 8 9 10
50 11 12 13 14 15 16 17
51 18 19 20 21 22 23 24
52 25 26 27 28 29 30 31

Im Gebäude S2|15 im
der TUD,
Abschnitt Stadtmitte Nord,
oder unter Anreise.

A A A | Print Drucken | Impressum Impressum | Contact Kontakt
    zum Seitenanfangzum Seitenanfang