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 TopTopics
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
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 TopImportant 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 |
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) |
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