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.
News
Submission to the Numerical Software Verifiction special issue of MCS is now closed.
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 (Dutton-Ducoffe Professor of Aerospace Engineering, 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 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. 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.
Benchmarks
Simple programs:- Absorption
- Middle
- Golden number : A and B
- Associativity
- Normalisation
- Polynomial
- Interpolation : A and B
- Inversion
- Filter
- cav10
Important Dates
Abstract submission deadline: April 2, 2010.
Paper submission deadline: April 9, 2010.
Notification of acceptance/rejection: April 28, 2010.
Worshop: July 15, 2010.
MSC special issue paper submission deadline (extended): November 15, 2010.
Program
08:25-08:30 |
Organizers |
Opening |
08:30-09:30 |
Sylvie Boldo |
Formal verification of numerical programs: from C annotated programs to Coq proofs, slides, photo |
9:30-10:00 |
Pieter Collins, Milad Niqui and Nathalie Revol |
A Taylor Function Calculus for Hybrid System Analysis: Validation in Coq. slides |
10:00-10:30 |
Coffee Break |
|
10:30-11:00 |
Vijay D'Silva, Leopold Haller and Daniel Kroening |
SMT-Style Program Analysis with Value-based Refinements. slides, photo
|
11:00-11:30 |
Stef Graillat, Fabienne Jézéquel and Yuxiang Zhu |
Stochastic Arithmetic in Multiprecision. slides |
11:30-12:00 |
Hong Diep Nguyen and Nathalie Revol |
Doubling the precision for the residual and the solution in interval iterative refinement for linear system solving and certifying. slides, photo |
12:00-12:30 |
Vijay D'Silva |
Properties Provable with Abstract Domains. , photo, photo |
12:30-13:30 |
Lunch |
|
13:30-14:30 |
Eric Feron |
Applications of control to formal software semantics, slides.ppt or slides.pdf, photo |
14:30-15:00 |
Stephen F. Siegel, Timothy Zirkel and Yi Wei |
A Functional Equivalence Verification Suite for High-Performance Scientific Computing. slides.pdf, photo |
15:00-15:30 |
Coffee Break |
|
15:30-16:00 |
Stephen F. Siegel, Yi Wei and Timothy Zirkel |
The Toolkit for Accurate Scientific Software. slides |
16:00-17:30 |
All |
Tool competition:
|
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)