Registration is open.
To register to the NSV workshop and other FLOC events, please go here: http://vsl2014.at/registration/.
Numerical computations are ubiquitous in digital 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. To achieve the verification and validation of global properties, numerical techniques need to precisely represent local behaviors of each component. In fact, in numerical algorithms, coarse abstractions are unlikely to succeed essentially because of the above mentioned issue. The implementation of numerical techniques on modern hardware adds another layer of approximation because of the use of finite representations of infinite precision numbers that usually lack basic arithmetic properties such as commutativity and associativity. It is hence imperative to develop logical and mathematical techniques that would allow reasoning about programmability and reliability. The NSV workshop is dedicated to the current development and the future prospects for such techniques. 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 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
- Trade-offs between quality of service and resource (for example energy) consumption in programs
- Benchmarks and tools for numerical software verification
The NSV 2014 program committee is:
ProgramA preliminary program is available here.
- Jean-Michel Muller. Getting tight error bounds in floating-point arithmetic: illustration with complex functions, and the real x^n function
Abstract: The specifications provided by the IEEE 754 standard for floating-point arithmetic allows one to design very simple algorithms for functions such as $x^n$, or complex multiplication and division, that are much more accurate that what one might think at first glance. We will show how tight error bounds are obtained for these algorithms, and discuss how generic exemples can be built to show the tightness of these error bounds.
- Sumit Kumar Jha. Verifying Parameterized Software Models in Computational IData Science against Behavioral Specifications
Abstract: Computational data science uses a variety of numerical software models to understand, predict and control the evolution of complex systems. For example, computational systems biology employs multi-scale mechanistic stochastic rule-based models while culturomics uses detailed agent-based models. Because of the inherent uncertainty involved in precisely measuring natural systems, software models employed in computational data science include a number of unknown or imprecisely known parameters. A fundamental problem in developing such software models is to discover the set of parameter values that enable a computational model to satisfy a given set of behavioral specifications. In this talk, we will present a new massively parallel extreme-scale parameter discovery algorithm for complex intelligent software models. We will discuss preliminary results obtained using a parallel implementation of the algorithm on a small 1,792-core CUDA cluster. The talk will also identify opportunities for future research in verifying numerical software being deployed by computational data scientists.
- Jim Kapinski. Numerical Challenges in Simulation-guided Dynamical System Analysis
Abstract: Verification and validation (V&V) for industrial control designs can be a difficult and expensive process. Simulation-guided approaches offer a practical means of performing V&V for industrial applications. One such technology uses simulation traces to discover Lyapunov functions or barrier certificates. This technique has proved promising; however, there are challenges related to the numerical computations involved. For example, the technique translates data obtained from simulation traces into a large collection of linear constraints, but not all of these constraints are necessarily useful for solving the problem. Strategies for selecting an appropriate subset of these constraints are required. In this talk, we present an overview of the simulation-guided analysis approach and discuss these numerical challenges.
- 2013, April 8, 2013, Philadelphia, Pennsylvania, collocated with CPSWeek 2013
- 2012, July 7-8, 2012, Berkeley, California, collocated with CAV 2012
- 2011, July 14, 2011, Salt lake City, Utah, collocated with CAV 2011
- 2010, July 15, 2010, Edinburgh, UK, collocated with the Federated Logic Conference FLoC 2010
- 2009, April 16, 2009, San Fransisco, California collocated with CPSWeek 2009
- 2008, July 8, 2008, Princeton, New Jersey, collocated with CAV 2008