NSV 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. This paper presents a program transformation that removes square roots and divisions from functional programs without recursion, producing code that can be exactly computed. This transformation accepts different subsets of languages as input and it provides a certifying mechanism when the targeted language is Pvs. In this case, we provide a relation between every function definition in the output code and its corresponding one in the input code, that specifies the behavior of the produced function with respect to the input one. This transformation has been implemented in OCaml and has been tested on different algorithms from the NASA ACCoRD project.

ABSTRACT. Numerical programs performing floating-point computations are very sensible to the way formulas are written. Several techniques have been proposed concerning the transformation of expressions in order to improve their accuracy and now we aim at going a step further by automatically transforming larger pieces of code containing several assignments and control structures. This article presents a case study in this direction. We consider a PID controller and we transform its code in order to improve its accuracy. The experimental data obtained when we compare the different versions of the code (which are mathematically equivalent) show that those transformations have a significant impact on the accuracy of the computations.

ABSTRACT. The computational complexity of the certified iteration of discrete dynamical systems is considered. Relations to the Lyapunov-Exponents are shown.

ABSTRACT. This work outlines an equation-based formulation of a digital control program and transducer interacting with a continuous physical process, and an approach using the Coq theorem prover for verifying the performance of the combined hybrid system. Considering thermal dynamics with linear dissipation for simplicity, we focus on a generalizable, physically consistent description of the interaction of the real-valued temperature and the digital program acting as a thermostat. Of interest in this work is the discovery and formal proof of bounds on the temperature, the degree of variation, and other performance characteristics. Our approach explicitly addresses the need to mathematically represent the decision problem inherent in an analog-to-digital converter, which for rare values can take an arbitrarily long time to produce a digital answer (the so-called Buridan's Principle); this constraint ineluctably manifests itself in the verification of thermostat performance. Furthermore, the temporal causality constraints in the thermal physics must be made explicit to obtain a consistent model for analysis. We discuss the significance of these findings toward the verification of digital control for more complex physical variables and fields.

ABSTRACT. We prove in this paper that policy iteration can be generally defined in finite templates domain using Lagrange duality without any assumption on the templates. Such policy iteration algorithm always converges to a fixed point under a very simple technical condition. This fixed point furnishes a safe over-approximation of the set of reachable values taken by the variables of a program. The paper also discusses the choice of good templates and links these good templates to invariant algebraic relations. When templates are well chosen, policy iteration developed in this paper can be easily initialised for one single loop programs.