Fri, 06.10.2017, 13:30 
Formal Verification in Imperative Multivalued Programming over Continuous Data Types LogikSeminar Speaker: Prof. Dr. Martin Ziegler, KAIST Room: S215201 (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=nonextensional 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
Department of Mathematics
Logic Group
S215
Schloßgartenstraße 7
64289 Darmstadt
GERMANY
Phone: +49(0)61511622863
Fax: +49(0)61511622840
logik@mathematik.tudarmstadt.de
Secretary's office  
Office hours: 

Click on TUD locations,
section Center North (S2)
or see directions.