NSV on Thursday, July 15th

08:30‑09:30 Invited talk
Location: AT LT3
08:30 Sylvie Boldo (INRIA Saclay)
Formal verification of numerical programs: from C annotated programs to Coq proofs

Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and Coq. This requires the C program to be annotated: this means that each function must be precisely specified, and we will prove the correctness of the program by proving both that it meets its specifications and that it does not fail. Examples will be given to illustrate the features of this approach.

09:30‑10:00 Session 1
Location: AT LT3
09:30 Pieter Collins, Milad Niqui and Nathalie Revol
A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq (Extended abstract)

We present a framework for the verification of the numerical algorithms used in Ariadne, a tool for analysis of nonlinear hybrid system. In particular, in Ariadne, smooth functions are approximated by Taylor models based on sparse polynomials. We use the Coq theorem prover for developing Taylor models as sparse polynomials with floating-point coefficients. This development is based on the formalisation of an abstract data type of basic floating-point arithmetic . We show how to devise a type of continuous function models and thereby parametrise the framework with respect to the used approximation, which will allow us to plug in alternatives to Taylor models.

10:30‑12:30 Session 2
Location: AT LT3
10:30 Vijay D'Silva, Leopold Haller and Daniel Kroening
SMT-Style Program Analysis with Value-based Refinements

Verification with abstract domains is a powerful technique to prove program properties. Often, an analysis may fail because either the domain or the analysis loses crucial information about program behaviour. In this paper, we consider a recent approach that uses an SMT-like architecture to refine the control-flow information of the program under consideration. We describe ongoing work in extending this technique to cover a wider class of refinements. We propose a refinement based on variable values and contrast it with the existing procedure.

11:00 Stef Graillat, Fabienne Jézéquel and Yuxiang Zhu
Stochastic Arithmetic in Multiprecision

In the article we will present a library called SAM (Stochastic Arithmetic in Multiprecision). It is a multiprecision extension of the classic CADNA library. The CADNA library implements a stochastic arithmetic that makes it possible to estimate the propagation of rounding error in scientific codes. Concretely, each variable is replaced by three floating-point numbers and the rounding mode is chosen randomly. The figures that differ in these three numbers are due to rounding errors. The actual version of CADNA only deals with single and double precision numbers defining stochastic numbers in single and double precision. We have extended the library so as to we use multiprecision numbers. In CADNA the arithmetic and relational operators are overloaded in order to be able to deal with stochastic numbers. As a consequence, the use of CADNA in a scientific code needs only few modifications.

The MPFR Library defines types of multiprecision numbers as well as arithmetic functions acting on multiprecision variables. What is important is that MPFR provides correctly rounded functions and operators in multiprecision. We have embedded MPFR into CADNA. This new library SAM makes it possible to dynamically control the numerical methods used and more particularly to determine the optimal number of iterations in an iterative process. We will present some applications of SAM in the numerical validation of chaotic systems.

11:30 Hong Diep Nguyen and Nathalie Revol
Doubling the precision for the residual and the solution in interval iterative refinement for linear system solving and certifying

Solving and certifying the solution of a linear system is the problem addressed in this paper. The method employed here is based on iterative refinement (cf. chapter 12 of Higham "Accuracy and Stability of Numerical Algorithms", SIAM, 2002). Two ingredients are used to get a certified and accurate solution.

To get accurate results, the computing precision is doubled for the computation not only of the residual, but also of the solution itself, as advised in Demmel, Hida, Kahan, Li, Mukherjee and Riedy (ACM TOMS 2006, vol. 23, no 2). To get a certified solution. ie. a solution along with a guaranteed enclosure of the error, interval computations are performed. Last but not least, efficiency is also an issue: we stick to the paradigm that presides to IntLab (cf. http://www.ti3.tu-harburg.de/rump/intlab/): we perform as many floating-point computations as possible. To reach this goal, we have "relaxed" (ie. enlarged) the matrix of the preconditioned linear system.

We will present experimental results illustrating the accuracy and efficiency of the proposed method.

12:00 Vijay D'silva
Properties Provable with Abstract Domains.

Verification with abstract domains is a sound but incomplete method for reasoning about programs. Due to the undecidability of program verification, incompleteness is often assumed to be a necessary tradeoff. However, there may be restricted programming languages and specification logics for which an abstract domain admits complete reasoning. This work is concerned with extracting logics and language definitions from a given abstract domain. Such results explain when reasoning with a domain should succeed and explain the scope of techniques such as trace-partitioning. We derive these results by applying duality theorems that relate logics with their algebraic models.

13:30‑14:30 Invited talk
Location: AT LT3
13:30 Eric Feron (Dutton-Ducoffe Professor of Aerospace Engineering, Georgia Institute of Technology)
Applications of control to formal software semantics

One of the primary purposes of embedded software and systems is to implement control algorithms aimed at harnessing the dynamics of complex dynamical systems, such as aircraft, automobiles, fast trains and automated transit systems. The necessity to certify these systems makes it a requirement to extract the semantics of the software as it interacts with the physical world. Several tools exist to achieve that goal, and they have displayed excellent performance when applied to large safety-critical software such as that present in avionics systems. This presentation will be devoted to the contributions that control theory may bring to the extraction of useful control software semantics. It will be shown by means of examples that the process by which such semantics is obtained may be greatly simplified when working with control system specifications first. Numerical issues that arise when moving from the ideal world of system specifications to the concrete software environment will also be discussed.

14:30‑15:00 Session 3
Location: AT LT3
14:30 Stephen F. Siegel, Timothy Zirkel and Yi Wei
A Functional Equivalence Verification Suite for High-Performance Scientific Computing

Scientific computing poses many challenges to formal verification, including the facts that typical programs (1) are numerically-intensive, (2) are highly-optimized (often by hand), and (3) often employ parallelism in complex ways.

Another challenge is specifying correctness. One approach is to provide a very simple, sequential version of an algorithm together with the optimized (possibly parallel) version. The goal is to show the two versions are functionally equivalent, or provide useful feedback when they are not.

We present a new verification suite consisting of pairs of programs of this form. The suite can be used to evaluate and compare tools that verify functional equivalence. The programs are all in C and the parallel versions use the Message Passing Interface. They are simpler than codes used in practice, but are representative of real coding patterns (e.g., manager-worker parallelism, loop tiling) and present realistic challenges to current verification tools. The suite includes solvers for the 1-d and 2-d diffusion equations, laplace iteration schemes, Gaussian elimination, and N-body simulation.

15:30‑16:00 Session 4
Location: AT LT3
15:30 Stephen F. Siegel, Yi Wei and Timothy Zirkel
The Toolkit for Accurate Scientific Software

The Toolkit for Accurate Scientific Software (TASS) is a suite of integrated tools for the formal verification of programs used in computational science, including numerically-intensive message-passing-based parallel programs. While TASS can verify a number of standard safety properties (such as absence of deadlocks and out-of-bound references), its most powerful feature is the ability to establish that two programs are functionally equivalent. These properties are verified by performing an explicit state enumeration of a model of the program(s). In this model, symbolic expressions are used to represent the inputs and the values of variables. In many cases, TASS can even verify the equivalence of programs with unbounded loops, using novel symbolic execution techniques. The TASS front-end supports a large subset of C, including (multi-dimensional) arrays, structs, dynamically allocated data, pointers and pointer arithmetic, functions and recursion, and other commonly used language constructs.