On Formal Verification in Imperative Multivalued Programming over Continuous Data Types.
Norbert Müller, S. Park, Norbert Preining, Martin Ziegler · arXiv (Cornell University) · 2016
Using fundamental ideas from [Brattka&Hertling'98] and by means of object-oriented overloading of operators, the iRRAM library supports imperative programming over the reals with a both sound and computable, multivalued semantics of tests. We extend Floyd-Hoare Logic to formally verify the correctness of symbolic-numerical algorithms employing such primitives for three example problems: truncated binary logarithm, 1D simple root finding, and solving systems of linear equations. This is to be generalized to other hybrid (i.e. discrete and continuous) abstract data types.