Numerical computations are ubiquitous in cyber-physical systems: supervision, prediction, simulation and signal processing rely heavily on numerical calculus to achieve desired goals. Verification of numerical algorithms has a unique set of challenges, which set it apart from rest of software verification. While verification and validation of software target global properties of the whole system, numerical techniques intrinsically focus on local considerations or approximations of system components. While “ abstracting away ” the data can still give meaningful proofs of correctness for many types of software, in numerical algorithms, such abstractions are unlikely to succeed. The implementation of numerical techniques on modern hardware adds another layer of approximation because of the use of finite representations of infinite precision numbers. Such representations usually lack basic arithmetic properties such as commutativity and associativity, and can cause catastrophic variations in the global system behavior through something as innocuous as a rounding error. It is hence imperative to develop logical and mathematical techniques that would allow reasoning about programmability and reliability in this space. The NSV workshop is dedicated to the current development and the future prospects for such techniques.


The topics of the workshop include, but are not restricted to, the following items.

  • Models and abstraction techniques
  • Specifications of correctness for numerical programs
  • Formal specification and 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 space, avionics, automotive and real-time applications
  • Validation for scientific computing programs
  • Optimality of program behavior
  • Tradeoffs between quality of service and resource (for example energy)
  • consumption in programs
  • Benchmarks and tools for numerical software verification

Submission Guidelines

We welcome submissions covering one or multiple areas of the workshop's topics.

Regular papers, 15 pages, Springer LNCS format.

Tool, Benchmark and Case-studies papers, 6 pages, Springer LNCS format.

Extended abstract (work in progress), 5 pages Springer LNCS format.

The submissions should not exceed the limit number of pages mentionned above including the bibliography. Instructions, style files and examples of the Springer LNCS format can be found here . All submissions should be made through the NSV easychair website.

Authors of selected papers will be invited to submit a final extended version to a special issue of the journal Mathematics in Computer Science.

Important Dates

  • Submission deadline Friday, February 1st, 2013 -- Extended Sunday, February 17th, 2013, AoE
  • Notification March 2nd 2013
  • Final version March 8th 2013


Khalil Ghorbal Carnegie Mellon University
Jyotirmoy V. Deshmukh Toyota Technical Center

Program Committee

Swarat Chaudhuri Rice University
Sriram Sankaranarayanan University of Colorado, Boulder
Eric Goubault CEA-LIST/École Polytechnique
Sylvie Putot CEA-LIST/École Polytechnique
Franjo Ivančić NEC Laboratories America
Jim Kapinski Toyota Technical Center


For questions related to this workshop please contact the organizers.


We are grateful to Maplesoft for its support.




The preliminary program of the workshop is now available.

Early registration for the NSV Workshop ends by March 8th 2013, you can register here then select the workshop (W8).

Selected work (paper or presentation) may win a one-year professional license of Maplesoft !

By popular demand, last deadline extension: Sunday, February 17th, 2013, AoE

Arnaud J. Venet (CMU & NASA) will be an invited speaker for this edition.

Ashish Tiwari (CSL SRI) will be an invited speaker for this edition.

Alexandre Donzé (UC Berkeley) will be an invited speaker for this edition.