NSV-3: July 15

Overview

The NSV workshop is dedicated to the current development and future prospects on applying logical and mathematical techniques for reasoning about numerical aspects of software. The scope of the workshop includes, but is not restricted to, the following topics:

• Models and Abstraction Techniques,
• Specifications of correctness for numerical programs
• Formal verification of numerical programs,
• Quality of finite precision implementations,
• Propagation of uncertainties, deterministic and probabilistic models,
• Numerical properties of control software,
• Hybrid systems verification,
• Validation for avionics, automotive and real-time applications.
• Validation for scientific computing programs
• Benchmarks and tools for numerical software verification

More information can be found here.

Program

• Accepted Papers
• Program

Invited Talks

• 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.
• 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.

Program Chairs

Program Committee: