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.



Fachbereich Mathematik
Technische Universität Darmstadt

Schlossgartenstraße 7
64289 Darmstadt

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