Sewon Park: Formal Verification in Imperative Multivalued Programming over Continuous Data Types

Sewon Park
Korea Advanced Institute of Science and Technology

Abstract: 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.

This is joint work with Gyesik Lee, Norbert Müller, Eike Neumann, Sewon Park, Norbert Preining and Martin Ziegler.