<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><div><br></div><div>&nbsp;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp;CALL FOR PAPERS<br><br><div>------------------------------------------------------------------------------------------------------<br>NSV-2011 : Fourth International Workshop on Numerical Software Verification.<br>&nbsp;&nbsp; &nbsp; &nbsp; &nbsp;&nbsp;<a href="http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV-2011">http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV-2011</a><br><br>&nbsp;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; &nbsp; Cliff Lodge, Snowbird, Utah, July 14, 2011.</div><div><br>Associated to Computer Aided Verification CAV 2011&nbsp;<br>(<a href="http://www.cs.utah.edu/events/conferences/cav2011/">http://www.cs.utah.edu/events/conferences/cav2011/</a>), July 14-20, 2011.&nbsp;</div><div>------------------------------------------------------------------------------------------------------<br><br>Overview<br>------------<br>The fourth workshop on Numerical Software Verification (NSV-2011) will be held<br>in Cliff Lodge, Snowbird, Utah, on July 14, 2011, and associated to the&nbsp;<br>Conference on Computer Aided Verification CAV 2011.<br><br>Topics<br>---------<br>The NSV workshop is dedicated to the current development and future prospects<br>on applying logical and mathematical techniques for reasoning about numerical<br>aspects of software. The workshop will also be an occasion to discuss robustness&nbsp;<br>of software and systems under uncertainty of values and numerical perturbations,&nbsp;<br>which is a central issue in numerical methods and robust control.&nbsp;<br>The scope of the workshop includes the following topics:<br><br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Models and Abstraction Techniques,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Specifications of correctness for numerical programs<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Formal verification of numerical programs,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Quality of finite precision implementations,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Propagation of uncertainties, deterministic and probabilistic models,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Numerical properties of control software,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Robustness of software and systems,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Analyses for functional properties: continuity, differentiability,<br>stability, robustness and well-conditioning,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Hybrid systems verification,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Validation for avionics, automotive and real-time applications.<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Validation for scientific computing programs<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Benchmarks and tools for numerical software verification<br><br>Submissions<br>-----------------<br>One aim of the workshop is to constitute a library of benchmarks for numerical<br>programs. We thus invite researchers of the field to submit not only original<br>research papers, but also benchmarks and tool papers. We will propose a very<br>informal and relaxed tool contest during the workshop, partially based on the<br>submitted benchmarks papers. Please inform us 3 weeks before the workshop of&nbsp;<br>your intention to participate. We encourage tool writers to submit a tool paper,&nbsp;<br>but if not please send us at least 3 weeks before a short description of your tool&nbsp;<br>(in particular properties verified, language for the benchmarks, platform for installation).<br><br>We call for several categories of submissions (via easychair, see the web page<br>of the workshop&nbsp;<a href="http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV-2011">http://www.lix.polytechnique.fr/Labo/Sylvie.Putot/NSV-2011</a>):<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Regular original papers, not exceeding 15 pages using Springer's<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;LNCS format<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Extended abstracts, 5 pages using Springer's LNCS format<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(work in progress)<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Benchmark papers, not exceeding 6 pages using Springer's LNCS format,<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;describing test programs along with expected properties and results,<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Tool papers, not exceeding 6 pages using Springer's LNCS format, and<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;the intention (by email to the organizers) to participate or not in an<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;informal tool contest on the benchmarks.<br><br>Final proceedings will be edited after the workshop, most probably as a special issue&nbsp;<br>of ENTCS or Mathematics in Computer Science. This special issue will undergo&nbsp;<br>the classical reviewing process.<br><br>Important dates<br>---------------------<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Paper submission deadline: March 31, 2011.<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Notification of acceptance/rejection: May 6, 2011.<br>- &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;Workshop: July 14, 2011.<br><br>Workshop Organizers<br>-----------------------------<br>Eric Goubault (CEA LIST, France)<br>Sylvie Putot (CEA LIST, France)<br>Stefan Ratschan (Academy of Sciences, Czech Republic)<br>Sriram Sankaranarayanan (University of Colorado Boulder)<br><br>Program Committee<br>---------------------------<br>Sylvie Boldo &nbsp;(INRIA Saclay - Proval)<br>Swarat Chaudhuri (Pennsylvania State University)<br>Michael Colon (U.S. Naval Research Laboratory)<br>Eric Feron (Georgia Institute of Technology)<br>Stéphane Gaubert (INRIA Saclay - MaxPlus)<br>Nathalie Revol (INRIA - Arénaire)<br>Stephen F. Siegel (University of Delaware)</div></div></body></html>