NSV-3: Third International Workshop on Numerical Software Verification.
July 15th, 2010.
Part of Federated Logic Conference FLoC 2010,
Edinburgh, 9-21 July, 2010.
Edinburgh, 9-21 July, 2010.
Introduction
The third workshop on Numerical Software Verification (NSV) will be held in Edinburgh, Scotland, on July 15th, 2010 . It will be part of the Federated Logic Conference FLoC 2010 and will be affiliated with the Conference on Computer Aided Verification CAV 2010 and the Symposium on Logic in Computer Science LICS 2010. This workshop will continue along the lines of NSV-I (2008) that was held in July 2008 along with CAV 2008 at Princeton, NJ, and NSV-II (2009), held in April 2009 as part of CPSWeek'09, and affiliated with the conference on Hybrid Systems: Computation and Control.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 scope of the workshop includes, but is not restricted to, 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,
- 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
Sylvie Boldo (INRIA Saclay)
Eric Feron (Georgia Institute of Technology)
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. If you have any problems, please contact the organizers.
Authors of selected papers will be invited to submit a final version to a special issue of the journal Mathematics in Computer Science.
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
Abstract submission deadline: March 25, 2010.
Paper submission deadline: April 1, 2010.
Notification of acceptance/rejection: April 28, 2010.
Worshop: July 15, 2010.
MSC special issue paper submission deadline (tentative): October 1, 2010.
Organizers
Georgios Fainekos (Arizona State University)
Eric Goubault (CEA LIST)
Sylvie Putot (CEA LIST)
Program Committee
Rajeev Alur (University of Pennsylvania)
Martin Berz (Michigan State University)
Stéphane Gaubert (INRIA Saclay - MaxPlus)
Alwyn E. Goodloe (National Institute of Aerospace)
Franjo Ivancic (NEC Laboratories America)
Guillaume Melquiond (INRIA Saclay - Proval)
David Monniaux (CNRS - VERIMAG)
Stefan Ratschan (Academy of Science of the Czech Republic)
Nathalie Revol (INRIA - Arénaire)
Sriram Sankaranrayanan (University of Colorado Boulder)
Hakan Yazarel (Toyota)
