[TYPES/announce] NSV 2015 - Call for participation

[Sergiy Bogomolov]

CALL FOR PARTICIPATION

**************
NSV 2015
**************

8th  International Workshop on Numerical Software Verification
April 13, 2015
Cyber-Physical Week  2015
Seattle, WA, USA

Web Page: http://nsv2015.informatik.uni-freiburg.de/

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

Registration
===========================

http://www.cpsweek.org/2015/reg.html (Regular registration rates until
April 7, 2015)

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
TBA, Numerical challenges for Maple (Remote talk)

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

* Daisuke Ishii, Naoki Yonezaki and Goldsztejn Alexandre. Monitoring
Bounded LTL Properties Using Interval Analysis

* 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

RTSS Panel and Reception 17-18:30