NSV 2014 - 7th International Workshop on Numerical Software Verification

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.