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:

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:

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).

Benchmarks

Simple programs: Some programs dedicated to floating-point computations, provided by Nathalie Revol: Annotated programs, provided by Sylvie Boldo: FEVS, a functional equivalence verification suite from the Verified Software Laboratory

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)

Contact

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

Sponsors

We are grateful to CEA List for their support.

LIST