From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id BA4477EEAF for ; Thu, 31 Jan 2013 22:02:44 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of khalil.ghorbal@gmail.com) identity=pra; client-ip=209.85.214.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="khalil.ghorbal@gmail.com"; x-sender="khalil.ghorbal@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of khalil.ghorbal@gmail.com designates 209.85.214.47 as permitted sender) identity=mailfrom; client-ip=209.85.214.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="khalil.ghorbal@gmail.com"; x-sender="khalil.ghorbal@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f47.google.com) identity=helo; client-ip=209.85.214.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="khalil.ghorbal@gmail.com"; x-sender="postmaster@mail-bk0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkgCAKzaClHRVdYvjWdsb2JhbABFFoVYWoEbtz0IFg4BAQEBCQkLCRIGI4IxEQYdARsMEgMSAw03AiQBEQEFASITh34BAw8MlDyMK4Jwi2VPgnuEZgoZJw1ZiHcBBQyNBYJogRMDiGSNLo5rFimEO4FKBxcG X-IPAS-Result: AkgCAKzaClHRVdYvjWdsb2JhbABFFoVYWoEbtz0IFg4BAQEBCQkLCRIGI4IxEQYdARsMEgMSAw03AiQBEQEFASITh34BAw8MlDyMK4Jwi2VPgnuEZgoZJw1ZiHcBBQyNBYJogRMDiGSNLo5rFimEO4FKBxcG X-IronPort-AV: E=Sophos;i="4.84,579,1355094000"; d="scan'208";a="894452" Received: from mail-bk0-f47.google.com ([209.85.214.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 31 Jan 2013 22:02:44 +0100 Received: by mail-bk0-f47.google.com with SMTP id jc3so1528588bkc.6 for ; Thu, 31 Jan 2013 13:02:43 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:x-received:date:message-id:subject:from:to :content-type; bh=adYaYBEGdVJ69RvvyyFfBEBeHPQqD1n3T69OMiBZx68=; b=aFl13B9k0HnVaJSFBJXsgJiSOOEXcNcHT1p9ys0weiyXs49P2TQX22Kt/2p9pPnCZ8 RD0mDiTMF6dJez4fccrcJEdmIgTbnKdUtPT0ri3j3Ebw+wu6MhuCwwG650pXsM3P8nBp 60sxxA1dmDQZ0cGd2uyiZF1LPfsCPk+LIKrKEpAtPNIUQNUtOX2ovgARG38iXCr7WD68 B0Preu6Thcz8Jxdp/sR9F0QWLVYv+koXNWagKHWKmS17W4Ck+i5PM1w2RUDzIjZcRHR9 tfKjcWk/PWoTYeMeemt08JtjHgqpWROE7KRHocKHo+Z70+phX6kQA72LBfCRHpUT8WBn doKA== MIME-Version: 1.0 X-Received: by 10.204.157.152 with SMTP id b24mr2574483bkx.92.1359666163562; Thu, 31 Jan 2013 13:02:43 -0800 (PST) Received: by 10.205.44.71 with HTTP; Thu, 31 Jan 2013 13:02:42 -0800 (PST) Date: Thu, 31 Jan 2013 16:02:42 -0500 Message-ID: From: Khalil Ghorbal To: "jyotirmoy.deshmukh@tema.toyota.com" Content-Type: multipart/alternative; boundary=0015175df152b13d1f04d49bf2fa X-Validation-by: khalil.ghorbal@gmail.com Subject: [Caml-list] NSV 2013, CFP, Extended Deadline --0015175df152b13d1f04d49bf2fa Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable [my apologizes for multiple postings] CALL FOR PAPERS ************ NSV 2013 ************ 6th Workshop on Numerical Software Verification, A Satellite Workshop of the CPSWeek 2013 Philadelphia, Pennsylvania, USA April 8th 2013 http://www.lix.polytechnique.fr/~ghorbal/NSV-2013/ *Extended Deadline* =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D The submission deadline is extended to *February 8th 2013*. Important Dates =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Submissions deadline: *Friday, February 8th, 2013, AoE*. Notification: February 28th 2013. Final version: March 6th 2013. Description of the workshop =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D Numerical computations are ubiquitous in cyber-physical systems: supervision, prediction, simulation and signal processing rely heavily on numerical calculus to achieve desired goals. Verification of numerical algorithms has a unique set of challenges, which set it apart from rest of software verification. While verification and validation of software target global properties of the whole system, numerical techniques intrinsically focus on local considerations or approximations of system components. While =E2=80=9C abstracting away =E2=80=9D the data can still give meaningf= ul proofs of correctness for many types of software, in numerical algorithms, such abstractions are unlikely to succeed. The implementation of numerical techniques on modern hardware adds another layer of approximation because of the use of finite representations of infinite precision numbers. Such representations usually lack basic arithmetic properties such as commutativity and associativity, and can cause catastrophic variations in the global system behavior through something as innocuous as a rounding error. It is hence imperative to develop logical and mathematical techniques that would allow reasoning about programmability and reliability in this space. The NSV workshop is dedicated to the current development and the future prospects for such techniques. Topics =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D The topics of the workshop include: - Models and abstraction techniques - Specifications of correctness for numerical programs - Formal specification and 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 space, avionics, automotive and real-time applications - Validation for scientific computing programs - Optimality of program behavior - Tradeoffs between quality of service and resource (for example energy) - consumption in programs - Benchmarks and tools for numerical software verification Submission information =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D We solicit regular research papers about recent work under the wide umbrella of Numerical Software Verification detailed above. The submission should not exceed 15 pages, Springer LNCS format. We also welcome tool, benchmark and case-studies papers of at most 6 pages. Extended abstract describing work in progress of no more than 5 pages are also highly encouraged. More information about the submission guidelines can on the workshop website. All accepted submissions will be included in the CPSWeek CD-ROM. After the workshop, presenters of selected research papers will be invited to submit an extended version to a special issue about Numerical Software Verification of the journal of Mathematics in Computer Science. Papers should be submitted (as PDF) through easychair https://www.easychair.org/conferences/?conf=3Dnsv2013 Organizers =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Khalil Ghorbal, Logical Systems Lab, CS Department, Carnegie Mellon University Jyotirmoy V. Deshmukh, Toyota Technical Center All questions about the workshop can be addressed to them via email: Khalil.Ghorbal@polytechnique.edu Jyotirmoy.Deshmukh@tema.toyota.com Program Committee =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D - Khalil Ghorbal Carnegie Mellon University - Jyotirmoy V. Deshmukh Toyota Technical Center - Swarat Chaudhuri Rice University - Sriram Sankaranarayanan University of Colorado, Boulder - Eric Goubault CEA-LIST/=C3=89cole Polytechnique - Sylvie Putot CEA-LIST/=C3=89cole Polytechnique - Franjo Ivan=C4=8Di=C4=87 NEC Laboratories America - Jim Kapinski Toyota Technical Center --0015175df152b13d1f04d49bf2fa Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

[my apologizes for multiple postings]
<= div>

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= CALL FOR PAPERS

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 ************
=C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 NSV 2013
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ************
=C2=A0 =C2=A0 =C2=A0 =C2=A06th Workshop on Numerical Software Veri= fication,

=C2=A0 =C2=A0 =C2=A0 =C2=A0 A Satellite = Workshop of the CPSWeek 2013
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Philadel= phia, Pennsylvania, USA

=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= April 8th 2013





Extended Deadline
=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
The subm= ission deadline is extended to February 8th 2013.


Important Dates
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Submissions de= adline: =C2=A0 Friday, February 8th, 2013, AoE.
Notificati= on: =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 February= 28th 2013.
Final version: =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0March 6th 2013.


Description of the workshop
=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
Numerical computations are ubiquitous in cyber-physical systems:=
supervision, prediction, simulation
and signal processing rely heavily on numerical calculus to achieve
desired goals.
Verification of numerical algorithms has a= unique set of challenges,
which set it apart from rest of softwa= re verification.

While verification and validation of software target gl= obal properties
of the whole system,
numerical techniqu= es intrinsically focus on local considerations or
approximations = of system components.
While =E2=80=9C abstracting away =E2=80=9D the data can still give mea= ningful proofs
of correctness for many types of software, in nume= rical algorithms,
such abstractions are unlikely to succeed.
The implementation of numerical techniques on modern hardware adds an= other
layer of approximation because of the use of finite representations of=
infinite precision numbers.
Such representations usual= ly lack basic arithmetic properties such as
commutativity
and associativity, and can cause catastrophic variations in the global=
system behavior through something as innocuous as a rounding err= or.

It is hence imperative to develop logical and = mathematical techniques
that would allow reasoning about programmability and reliability in th= is space.
The NSV workshop is dedicated to the current developmen= t and the future
prospects for such techniques.


Topics
=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D
The topics of the workshop include:

- Models and abstraction techniques
- Specif= ications of correctness for numerical programs
- Formal specification and 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 space, avioni= cs, automotive and real-time applications
- Validation for scient= ific computing programs
- Optimality of program behavior
- Tradeoffs between quality of service and resource (for example energ= y)
- consumption in programs
- Benchmarks and tools for= numerical software verification


Submission information
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D
We solicit regular research papers about= recent work under
the wide umbrella of Numerical Software Verifi= cation detailed above.
The submission should not exceed 15 pages,= Springer LNCS format.
We also welcome tool, benchmark and case-studies papers of at most 6 p= ages.
Extended abstract describing work in progress of no more th= an 5 pages
are also highly encouraged.
More information= about the submission guidelines can on the workshop website.

All accepted submissions will be included in the CPSWee= k CD-ROM.
After the workshop, presenters of selected research pap= ers will be
invited to submit
an extended version to a = special issue about Numerical Software Verification
of the journal of Mathematics in Computer Science.

Papers should be submitted (as PDF) through easychair


Organizers
=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D
Khalil Ghorbal, =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 Logical Systems Lab, CS Department, Carnegie
Mellon University
Jyotirmoy V. Deshmukh, =C2=A0Toyota Technical = Center

All questions about the workshop can be addressed to th= em via email:



Program Committee
=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
- Khalil Ghorbal =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0Carnegie Mellon University
- Jyotirmoy V. Deshmukh =C2=A0 = =C2=A0 =C2=A0 =C2=A0 Toyota Technical Center
- Swarat Chaudhuri =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 =C2=A0 Rice University
- Sriram Sankaranarayanan =C2=A0 = =C2=A0 =C2=A0 University of Colorado, Boulder
- Eric Goubault =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 = =C2=A0 CEA-LIST/=C3=89cole Polytechnique
- Sylvie Putot =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 CEA-LIST/=C3=89cole Polytechnique
- Franjo Ivan=C4=8Di=C4=87 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0NEC Laboratories America
- = Jim Kapinski =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0Toyota Technical Center

--0015175df152b13d1f04d49bf2fa--