NSV 2015: 8th International Workshop on Numerical Software Verification 2015

NSV 2015: 8th International Workshop on Numerical Software Verifictaion 2015 in Seattle, WA, USA
Image source: de.wikipedia.org/Seattle

Scope

Numerical computations are ubiquitous in digital systems: supervision, prediction, simulation and signal processing rely heavily on numerical calculus to achieve desired goals. Design and 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. 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. Finally, the development and analysis of cyber-physical systems (CPS) which involve the interacting continuous and discrete components pose a further challenge. It is hence imperative to develop logical and mathematical techniques for the reasoning about programmability and reliability. The NSV workshop is dedicated to the development of such techniques.

Back to Top

Topics

The scope of the workshop includes, but is not restricted to, the following topics:

  • Quantitative and qualitative analysis of hybrid systems
  • Models and abstraction techniques
  • Optimal control of dynamical systems
  • Parameter identification for hybrid systems
  • Numerical optimization methods
  • Hybrid systems verification
  • Applications of hybrid systems to systems biology
  • Propagation of uncertainties, deterministic and probabilistic models
  • Specifications of correctness for numerical programs
  • Formal specification and verification of numerical programs
  • Quality of finite precision implementations
  • Numerical properties of control software
  • Validation for space, avionics, automotive and real-time applications
  • Validation for scientific computing programs

Back to Top

Call for Papers

Call for papers can be found here:

Back to Top

Program

Invited talk: 8:30-9:20
Radu Grosu (Technical University of Vienna, Austria), Abstractions for Hybrid Systems

Session 1: 9:20-10:00 - Accurate Computing with Floating-Point Arithmetic (Session chair: Nasrine Damouche)

  • Sylvie Boldo. Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number
  • Stef Graillat, Fabienne Jézéquel and Romain Picot. Numerical validation of compensated summation algorithms with stochastic arithmetic

Coffee-break: 10:00-10:30

Session 2: 10:30-12:00 - Hybrid Systems Analysis (Session chair: Ian Michell)

  • Shota Matsumoto, Fumihiko Kono, Teruya Kobayashi and Kazunori Ueda. HyLaGI: Symbolic Implementation of a Hybrid Constraint Language HydLa
  • Miriam García Soto and Pavithra Prabhakar. AVERIST Algorithmic Verifier of Stability
  • Indranil Saha. Program Analysis and Synthesis for Control Software

Lunch-break: 12:00-13:00

Invited talk: 13:00-13:50
Andreas Griewank (Humboldt University of Berlin, Germany), Numerical Methods for Nonsmooth Problems based on Algorithmic Piecewise Differentiation

Session 3: 13:50-14:30 - Design and Modelling of Hybrid Systems (Session chair: Pavithra Prabhakar)

  • Nikos Arechiga, James Kapinski, Jyotirmoy Deshmukh, Andre Platzer and Bruce Krogh. Numerically-aided Deductive Safety Proof for a Powertrain Control System
  • Ashish Tiwari. Attacking a Feedback Controller

Coffee-break: 14:30-15:00

Invited talk: 15:00-15:40
Taylor T. Johnson (University of Texas at Arlington, USA), Real-Time Reachability for Verified Simplex Design

Session 4: 15:40-16:40 - Numerical Verification (Session chair: Sylvie Boldo)

  • Best Talk Award: Daisuke Ishii, Naoki Yonezaki and Goldsztejn Alexandre. Monitoring Bounded LTL Properties Using Interval Analysis
  • Best Talk Award: Charles Jacobsen, Alexey Solovyev and Ganesh Gopalakrishnan. A Parameterized Floating Point Formalization in HOL Light
  • Wei-Fan Chiang, Ganesh Gopalakrishnan and Zvonimir Rakamaric. Unsafe Floating-point to Unsigned Integer Casting Check for GPU Programs

Conclusion and Best Talk Awards 16:40-17

Forum on Artifact Evaluation 17-18:30

Workshop dinner: We meet at 18:30 at the conference registration desk downstairs and go to Sullivan’s Steakhouse (621 Union Street, Seattle, WA 98101).

Back to Top

Important Dates

Paper submission DEADLINE EXTENDED: February 14, 2015
Author notification EXTENDED: March 3, 2015
Camery-ready version EXTENDED: March 15, 2015
Workshop April 13, 2015

Back to Top

Program Committee

Ezio Bartocci (Vienna University of Technology, Austria) Sergiy Bogomolov (IST Austria, Austria) - co-chair
Sylvie Boldo (INRIA, France) Olivier Bouissou (Mathworks, France)
Sean Gao (MIT, USA) Khalil Ghorbal (CMU, USA)
Eric Goubault (Ecole Polytechnique, France) Jim Kapinski (Toyota, USA)
Matthieu Martel (Université de Perpignan, France) - co-chair Ian Mitchell (UBC, Canada)
Jan Otop (IST Austria) Pavithra Prabhakar (IMDEA, Spain)
Walid Taha (Halmstadt University, Sweden, & Rice University, USA)

Back to Top

Local Organization

Nasrine Damouche (Université de Perpignan, France)

Back to Top

Sponsors

We gratefully acknowledge the support from the following sponsors:

Toyota Maplesoft Numalis

Back to Top

Previous Editions

  • 2014, July 17-18, 2014, Vienna, Austria, collocated with Vienna Summer of Logic 2014
  • 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
Back to Top