Mar. 27th, 2009 Program is announced.
Mar. 6th, 2009 Check out the list of invited speakers and accepted submissions. Program will appear very soon!
Feb. 18th, 2009 Register for the workshop here. Limited financial support for students is available!.

Feb. 18th, 2009 Limited financial support for students is available!.


The second workshop on Numerical Software Verification (NSV) will be held San Francisco, CA on April 16th, 2009 . The focus of the workshop for 2009 will be on the verification of software for Cyber-Physical Systems (CPS). It will be part of the Cyber-Physical Systems Week CPSWeek and will be affiliated with the conference on Hybrid Systems: Computation and Control. This workshop will continue along the lines of NSV-I (2008) that was held in July 2008 along with CAV 2008 at Princeton, NJ. Proceedings of this workshop appeared as a special issue in the journal Formal Methods in Systems Design.


Cyber-Physical Systems (CPS) refers to the class of systems that integrate (engineered) physical systems with computational and communication systems. Examples of CPS range from small scale systems, such as implanted medical devices or autonomous robots, to medium scale, such as automobiles and aircrafts, to large scale systems, for example, a power grid. A key component of every CPS is the underlying (distributed heterogeneous) software that controls a system or a system of systems. Numerical and logical errors in the software can have catastrophic results on the physical system. For over a decade, the hybrid systems community has been actively looking for solutions to the verification problem of CPSs by targeting mainly the interaction between the physical system and the software at the abstract logical level. However, this is not enough. Many well-known CPSs failures have been attributed to the existence of numerical errors and bugs in the software.

This workshop aims to initiate and catalyze work along such research directions by bringing together people from the hybrid systems, control and software verification communities. A secondary goal of NSV-II will be to create a benchmark problems library. In the past, similar benchmark libraries have been beneficial in accelerating the development of new theories and toolboxes in specific research areas, for example, SAT solvers.

Topics of Interest

We invite leading researchers to talk about the current development and future prospects on applying logical and mathematical techniques for reasoning about numerical aspects of software. The scope of the workshop includes, but is not restricted to, the following topics:

Submissions that target different aspects of verification and testing in the context of CPS software are especially welcome.

Invited Speakers


Please submit your papers through easychair. If you have any problems, please contact the organizers.

The workshop submissions will consist of an extended abstract. The expected length of the abstract is 3 pages, however submissions up to 15 pages in LNCS format or 8 pages in IEEE conference format will be considered.

Authors of extended abstracts selected by the program committee will be invited to submit a full paper to a special edition of a ACM Transactions in Embedded Computing Systems (TECS).

All submissions (extended abstracts as well as post-conference) will be subjected to stringent review process for technical merit and suitability to the theme by the program committee.

Important Dates

Abstract submission deadline (extended): 12th Feb, 2009 .
Decision date: 25th Feb, 2009.
TECS special issue paper submission deadline (hard): 30th Jun, 2009.
TECS special issue decision date: 30th Sep, 2009.




Opening Remarks


Martin Berz

Rigorous High Order Computation with Taylor Models and Its Applications.


Coffee Break



Thao Dang

Using Box Splines to Approximate Reachable Sets of Polynomial Systems


Laurent-Stéphane Didier, Chapoutot Alexandre and Villers Fanny

Range Estimation of Floating-Point Variables in Simulink Models.



Goran Frehse, Hitashyam Maka and Bruce Krogh

Verification of Floating Point Computations Using Polyhedral Domains





Paul Caspi

Formal Methods in Computerized Control Design: a Tentative Overview


Domitilla Del Vecchio, Rajeev Verma and Michael Hafner

Control of Hybrid Automata with Imperfect Mode Information Assuming Separation between Estimation and Control


Coffee Break



Mike Whalen

Formal Verification of Avionics Software in a Model-Based Development Process


Ashish Tiwari

Formally Analyzing Adaptive Flight Control


Coffee Break



Agung Julius

Trajectory based analysis of cyber-physical systems using approximate bisimulation


Nadir Matringe, Arnaldo Vieira Moura and Rachid Rebiha

Morphisms for Analysis of Hybrid Systems

This is an one-day post-conference workshop consisting of presentations based on submissions as well as from invited speakers. Each speaker will be expected to deliver a 25 minute talk. This will be followed by 5 minutes of audience interaction.


Eric Goubault (CEA LIST, France),
Georgios Fainekos and Sriram Sankaranarayanan (NEC Laboratories America).

Program Committee


Details on the registration for the workshop can be found here.

Limited registration support in a form of a scholarship will be available for students who would like to attend the workshop. To be eligible, you must be currently registered as a student, and register for our workshop.

Since the available funding is limited, the scholarships will be awarded based on academic merit. Please email the organizers with a CV listing your current academic work and also ask your academic advisor to send us an email certifying your academic status. The actual scholarship will be given in the form of reimbursement for the cost of registering for the workshop. The exact amount will be decided based on the participation.

Hotel and Travel

NSV-II is part of the CPSWeek 2009 which will be held in the Parc 55 Hotel in San Francisco, CA, USA. For information about San Francisco please visit Welcome to San Francisco.


For questions related to this workshop and abstract submission for talks please contact the organizers.


We are grateful to
NEC Laboratories and CEA List for their support.