NSV-2011: Fourth International Workshop on Numerical Software Verification.
July 14th, 2011.
Associated to Computer Aided Verification CAV 2011,
Cliff Lodge, Snowbird, Utah, July 14-20, 2011.
Cliff Lodge, Snowbird, Utah, July 14-20, 2011.
News
Tentative program is announced
Introduction
The fourth workshop on Numerical Software Verification (NSV)
will be held in Cliff Lodge, Snowbird, Utah, on July 14th, 2011 ,
and associated to the Conference on Computer Aided Verification
CAV 2011.
This workshop will continue along the lines of
NSV-I (2008)
that was held in July 2008 along with CAV 2008 at Princeton, NJ,
NSV-II (2009), held in April 2009 as part of CPSWeek'09,
and affiliated with the conference on Hybrid Systems: Computation and Control, and
NSV-III (2010), held in July 2010 as part of the Federated Logic Conferences
FLoC 2010,
affiliated with the Conference on Computer Aided Verification
CAV 2010 and the Symposium on Logic in Computer Science
LICS 2010.
Topics of Interest
The NSV workshop is dedicated to the current development and future prospects on applying logical and mathematical techniques for reasoning about numerical aspects of software. The workshop will also be an occasion to discuss robustness of software and systems under uncertainty of values and numerical perturbations, which is a central issue in numerical methods and robust control. The scope of the workshop includes the following topics:- Models and Abstraction Techniques,
- Specifications of correctness for numerical programs
- Formal verification of numerical programs,
- Quality of finite precision implementations,
- Propagation of uncertainties, deterministic and probabilistic models,
- Numerical properties of control software,
- Robustness of software and systems,
- Analyses for functional properties: continuity, differentiability, stability, robustness and well-conditioning,
- Hybrid systems verification,
- Validation for avionics, automotive and real-time applications,
- Validation for scientific computing programs,
- Benchmarks and tools for numerical software verification.
Invited Speakers
James Demmel (University of California at Berkeley)
Thomas Gawlitza (INRIA Rhônes-Alpes)
Goran Frehse (Verimag)
Submission
One aim of the workshop is to constitute a library of benchmarks for numerical programs. We thus invite researchers of the field to submit not only original research papers, but also benchmarks and tool papers.
We call for several categories of submissions:
- Regular original papers, not exceeding 15 pages using Springer's LNCS format,
- Extended abstracts, 5 pages using Springer's LNCS format (work in progress),
- Benchmark papers, not exceeding 6 pages using Springer's LNCS format, describing test programs (if possible in C or similar imperative programs) along with expected properties and results,
- Tool papers, not exceeding 6 pages using Springer's LNCS format, and the intention (by email to the organizers) to participate or not in an informal tool contest on the benchmarks.
Please submit your papers through easychair.
Final proceedings will be edited after the workshop, most probably as a special issue of ENTCS or Mathematics in Computer Science. This special issue will undergo the classical reviewing process.
The tool contest
We will propose a very informal and relaxed tool contest during the workshop, partially based on the submitted benchmarks papers. Please inform us 3 weeks before the workshop of your intention to participate. We encourage tool writers to submit a tool paper, but if not please send us at least 3 weeks before a short description of your tool (in particular properties verified, language for the benchmarks, platform for installation).- The submitted benchmarks (and if possible, an indication of some expected properties) will be available to all on the web page before the workshop day, so that tool authors know what to expect,
- We will add some benchmarks of our own, which will remain secret until the contest,
- Each tool author will operate his own tool on the benchmarks, if possible on local computers, under the supervision of the organizers.
Important Dates
Paper submission deadline: March 31, 2011.
Notification of acceptance/rejection: May 6, 2011.
Camera-ready version: May 24, 2011.
Worshop: July 14, 2011.
Organizers
Eric Goubault (CEA LIST)
Sylvie Putot (Cea LIST)
Stefan Ratschan (Academy of Sciences, Czech Republic)
Sriram Sankaranarayanan (University of Colorado Boulder)
Program Committee
Sylvie Boldo (INRIA Saclay - Proval)
Swarat Chaudhuri (Pennsylvania State University)
Michael Colon (U.S. Naval Research Laboratory)
Eric Feron (Georgia Institute of Technology)
Stéphane Gaubert (INRIA Saclay - MaxPlus)
Nathalie Revol (INRIA - Arénaire)
Stephen F. Siegel (University of Delaware)