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.

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

Submission Information

We solicit regular and short papers. Paper submission must be performed via the EasyChair system.

Regular papers must describe original work, be written and presented in English, and must not substantially overlap with papers that have been published or that are simultaneously submitted to a journal or a conference with refereed proceedings. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant.

Regular paper submissions should not exceed 15 pages in LNCS style, including bibliography and well-marked appendices. Program committee members are not required to read the appendices, and thus papers must be intelligible without them. Short papers are also welcome, they should present tools, benchmarks, case-studies or be extended abstracts of ongoing research. Short papers should not exceed 6 pages.

All accepted papers will be published as Lecture Notes in Computer Science (LNCS) with Springer Verlag.lncs

Call for Papers

The call for papers (ASCII) can be downloaded here.

Important Dates

Paper submission April 22, 2016 Deadline extension: May 29, 2016
Author notification June 8, 2016
Camery-ready version June 15, 2016
Workshop July 17-18, 2016

Program

Day 1 (Sunday, July 17)

Session 1 – Hybrid Systems Verification (Session chair: Yassamine Seladji)

09:00 – 10:00
Alessandro Abate.
Verification of smart energy systems on the cloud

10:00 – 10:30
Alexandre Chapoutot and Julien Alexandre Dit Sandretto.
Studying Sequences of Jumps in Hybrid Systems to Detect Zeno Phenomenon

Session 2 – Abstract State Spaces (Session chair: Sergiy Bogomolov)

11:00 – 12:00
Yassamine Seladji.
Reduce the Complexity of the Polyhedron Minimization Using the Max Plus Pruning Method

12:00 – 12:30
Assale Adje.
Best Talk Award: Proving properties on PWA Systems using Copositive and Semidefinite Programming

Session 3 – Numerical Codes (Session chair: Sylvie Boldo)

02:00 – 03-00
Behzad Samadi.
Model Based Automatic Code Generation for Nonlinear Model Predictive Control

03:00 – 03:30
Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern and Zachary Tatlock.
Toward a Standard Benchmark Format and Suite for Floating-Point Analysis

Session 4 – Industrial Applications (Session chair: Sergiy Bogomolov)

04:00 – 05:00
Thomas Heinz.
Falsification of dynamical systems – an industrial perspective

6:00: Workshop dinner at WVRST (near Hyatt). We will start walking there from the workshop venue shortly after 5pm.

Day 2 (Monday, July 18)

Session 1 – System Modelling (Session chair: Thomas Heinz)

09:00 – 10:00
Cesare Tinelli.
A Mode-aware Contract Language for Reactive Systems

10:00 – 10:30
Sidi Mohamed Beillahi, Umair Siddique and Sofiene Tahar.
Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory

Session 2 – Numerical Verification (Session chair: Alessandro Abate)

11:00 – 12:00
Eric Feron.
Credible autocoding of convex optimization algorithms

12:00 – 12:30
Sylvie Boldo.
Best Talk Award: Computing a correct and tight rounding error bound using rounding-to-nearest

Invited Speakers

Alessandro Abate (University of Oxford, UK)
Verification of networks of smart energy systems over the cloud

This talk advocates the use of formal methods to verify and
certifiably control the behaviour of computational devices interacting
over a shared infrastructure. We deal with an engineering platform of
multiple, interleaving and interacting complex and adaptive systems, a
network with issues of synchronisation and coordination, feedback from
couplings and interactions, and with a global behaviour that is
emergent from local dynamics. Formal techniques can provide compelling
solutions when safety-critical goals are on target, as well as for
general quantitative analysis and control synthesis problems.
Two applicative areas are elucidated, dealing respectively with
thermal loads and electricity-generating devices interacting over a
smart energy network and over a local power grid respectively. We
discuss the corresponding problems of energy management in smart
buildings, of demand-response on smart grids, and of frequency
stabilisation and grid robustness.

Thomas Heinz (Robert-Bosch GmbH, Germany)
Falsification of dynamical systems – an industrial perspective

Whenever formal verification of dynamical system models is not
applicable, e.g., due to the presence of black-box components,
simulation-based verification and falsification methods are promising
approaches to gain confidence in a system satisfying its
specification. With the introduction of robust semantics it is not
only possible to answer this question in the Boolean sense but to
quantify its truth. We illustrate a number of applications that are
interesting from an industrial perspective, and point out how
robustness could become even more versatile in the engineering
process.

Eric Feron (Georgia Institute of Technology, USA)
Credible autocoding of convex optimization algorithms

Credible autocoding is a process of generating proof-carrying code
from high-level models that has been in existence for many years. This
presentation will discuss credible autocoding for control
applications, with a particular emphasis on receding-horizon
controllers (also named model-predictive controllers). Following a
brief historical overview, a prototype autocoder for embedded convex
optimization algorithms developed at ONERA (France) and Georgia Tech
(US) will be discussed. Options for encoding code properties and
proofs, and their applicability and limitations will be detailed. A
short discussion about numerical errors induced by finite-precision
calculations will follow. This work is performed in collaboration with
ONERA and ENSEEIHT (Toulouse, France).

Behzad Samadi (Maplesoft, Waterloo, Ontario, Canada)
Model Based Automatic Code Generation for Nonlinear Model Predictive Control

This paper demonstrates a symbolic tool that generates C code for
nonlinear model predictive controllers. The optimality conditions are
derived in a quick tutorial on optimal control. A model based workflow
using MapleSim for modeling and simulation, and Maple for analysis and
code generation is then explained. In this paper, we assume to have a
control model of a nonlinear plant in MapleSim. The first step of the
workflow is to get the equations of the control model from MapleSim.
These equations are usually in the form of differential algebraic
equations. After converting the equations to ordinary differential
equations, the C code for the model predictive controller is generated
using a tool created in Maple. The resulting C code can be used to
simulate the control algorithm and program the hardware controller.
The proposed tool for automatic code generation for model predictive
controllers is open and can be employed by users to create their own
customized code generation tool.

Yassamine Seladji (University of Tlemcen, Algeria)
Reduce the Complexity of the Polyhedron Minimization Using the Max Plus Pruning Method

The polyhedral analysis is widely used for the static analysis of
programs, thanks to its expressiveness but it is also time
consuming. To deal with that, a sub-polyhedral analysis has been
developed which offers a good tread off between expressiveness and
sufficiency. This analysis is based on a set of directions which is
defined statically at the beginning of the analysis. The larger the
cardinality of the direction set, the higher the precision of the
result.. Even if the set of directions is big, the sub-polyhedral
analysis can be done in a linear time. The bottleneck is that to
construct the resulting polyhedron with a large number of constraints
(one constraints per direction) is time consuming. In this talk, we
present a minimization method that allows to deal with that, using the
max plus pruning method. We demonstrate the efficiency of our method
on some benchmarks. The first results are very encouraging.

Cesare Tinelli (University of Iowa, USA)
A Mode-aware Contract Language for Reactive Systems

Contract-based software development is a major methodology for
the development of safety- and mission-critical embedded systems.
Contracts are an effective mechanism to establish boundaries between
components, and can be used efficiently to verify global, system-level properties
by means of compositional reasoning techniques. A contract specifies
the assumptions a component makes on its environment, and the guarantees
it provides. Requirements in a component’s specification are often case-based,
with each case referring to a particular behavioral mode for the component.
This talk introduces CoCoSpec, a mode-aware assume-guarantee-based contract
language for embedded systems. CoCoSpec, which is built as an extension of
the synchronous data-flow language Lustre, lets users specify mode behavior
directly, thus preserving mode-specific information contained in (natural
language) system requirements. Mode-aware model checkers supporting CoCoSpec
can increase the effectiveness and scalability of compositional analysis techniques
based on the assume-guarantee paradigm. In particular, they can leverage
the fine-tunable abstraction mechanism provided by modes in order to selectively
abstract complex numerical operations by their contracts, thus facilitating
the verification of systems with numerical components. The talk presents
the CoCoSpec language and illustrates the benefits of mode-aware model-checking
on a case study involving a flight-critical avionics system. The evaluation uses Kind 2,
a collaborative, parallel, SMT-based model checker developed at
the University of Iowa that provides full support for CoCoSpec.

Organizers

IST Austria Université de Perpignan, France
IST_Austria_Logo up
Kansas State University, USA ARiSE – Austrian Society for Rigorous Systems Engineering
download RiSE_Logo-small1

 

Program Committee

PC chairs
Sergiy Bogomolov (IST Austria, Austria)
Matthieu Martel (Université de Perpignan, France)
Pavithra Prabhakar (Kansas State University, USA)

PC members
Stanley Bak (Air Force Research Laboratory Rome, USA)
Ezio Bartocci (Vienna University of Technology, Austria)
Sylvie Boldo (INRIA, France)
Olivier Bouissou (CEA, France)
Alexandre Chapoutot (ENSTA ParisTech, France)
Nasrine Damouche (Université de Perpignan, France)
Georgios Fainekos (Arizon State University, USA)
Mirco Giacobbe (IST Austria, Austria)
Eric Goubault (CEA, France)
Susmit Jha (University of California, Berkeley, USA)
Jim Kapinski (Toyota, USA)
Ian Mitchell (UBC, Canada)
Dejan Nickovic (AIT, Austria)
Corina Pasareanu (NASA Ames Research Center, USA)
Walid Taha (Halmstadt University & Rice University, Sweden)
Oleg Sokolsky (University of Pennsylvania, USA)
Mahesh Viswanathan (University of Illinois at Urbana-Champaign, USA)

Sponsors

Toyota_RED Maplesoft_logo.svg

Previous editions

2015, April 13, 2015, Seattle, USA, collocated with CPSWeek 2015
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