From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/203 Path: news.gmane.org!not-for-mail From: Miroslav Velev Newsgroups: gmane.science.mathematics.petri-nets,gmane.comp.mathematics.reliable-computing,gmane.comp.science.concurrency,gmane.science.mathematics.categories Subject: 2nd call for papers: CFV'09, deadline April 22 Date: Fri, 27 Mar 2009 15:38:15 -0500 Message-ID: <95bd0d720903271338q4f4c04b6vfb43073333ca2605@mail.gmail.com> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: multipart/mixed; boundary="===============0965603931==" X-Trace: ger.gmane.org 1238229259 21412 80.91.229.12 (28 Mar 2009 08:34:19 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 28 Mar 2009 08:34:19 +0000 (UTC) To: puml-list@cs.york.ac.uk, reliable_computing@interval.louisiana.edu, procos@jiscmail.ac.uk, concurrency@cwi.nl, categories@mta.ca, moca-announce@list.it.uu.se, jml@cs.iastate.edu, ccp Original-X-From: petrinet-bounces@informatik.uni-hamburg.de Sat Mar 28 09:35:35 2009 Return-path: Envelope-to: gsmp-petrinet@gmane.org Original-Received: from mailhost.informatik.uni-hamburg.de ([134.100.9.70]) by lo.gmane.org with esmtp (Exim 4.50) id 1LnU0t-0004CM-PE for gsmp-petrinet@gmane.org; Sat, 28 Mar 2009 09:35:35 +0100 Original-Received: from localhost (localhost [127.0.0.1]) by mailhost.informatik.uni-hamburg.de (Postfix) with ESMTP id A42D8B30; Sat, 28 Mar 2009 09:34:10 +0100 (CET) X-Virus-Scanned: amavisd-new at informatik.uni-hamburg.de Original-Received: from mailhost.informatik.uni-hamburg.de ([127.0.0.1]) by localhost (mailhost.informatik.uni-hamburg.de [127.0.0.1]) (amavisd-new, port 10024) with LMTP id UisMccWVlTTe; Sat, 28 Mar 2009 09:34:09 +0100 (CET) Original-Received: from mailhost.informatik.uni-hamburg.de (localhost [127.0.0.1]) by mailhost.informatik.uni-hamburg.de (Postfix) with ESMTP id 104B2B2C; Sat, 28 Mar 2009 09:34:01 +0100 (CET) X-Virus-Scanned: amavisd-new at informatik.uni-hamburg.de Original-Received: from mailhost.informatik.uni-hamburg.de ([127.0.0.1]) by localhost (mailhost.informatik.uni-hamburg.de [127.0.0.1]) (amavisd-new, port 10024) with LMTP id jlEXWA2g0zlV for ; Fri, 27 Mar 2009 21:45:19 +0100 (CET) X-policyd-weight: using cached result; rate: -8.4 X-Greylist: delayed 414 seconds by postgrey-1.32 at mailhost; Fri, 27 Mar 2009 21:45:19 CET Original-Received: from mail-qy0-f126.google.com (mail-qy0-f126.google.com [209.85.221.126]) by mailhost.informatik.uni-hamburg.de (Postfix) with ESMTP id 0B9A63B6 for ; Fri, 27 Mar 2009 21:45:12 +0100 (CET) Original-Received: by qyk32 with SMTP id 32so2123142qyk.2 for ; Fri, 27 Mar 2009 13:45:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:received:date:message-id:subject :from:to:content-type; bh=MzlbD3645Zhp+oUTpIQ1MJFh6wAi9J5P6QdtWTjkh+g=; b=KaWdQ/7a2NDCXOv8FOaSbCQyyH35yBUIVhOT8+7yE9wR6qD1//CKSaX+u50Z6/BVpV HRi4zQbTG0dRgMBXqyQxpn9rAtOhrdvL5a8rFRCduYmEbM8r5nPb18fUd5c9bWAjvFqZ SiC9TFOnkXxOVENFiDJjhK//0yJSHcEJ6O3+0= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=T5L0eqJFbOdyFcMZt0Z9wA6SnAwyNckXldpGc4lziESjaGw53m/tgxwHevz4TYWFd1 QaPUlwct0Rx/tZhNGovVph3RSOCRiiMcDWs7Xkc1RKb1vXAbDmHNNncBmIeDDDq/0xoF umM+3Sq2J5XvAtPfhTKL70pXScyItlfd7ji8I= Original-Received: by 10.229.98.195 with SMTP id r3mr1219945qcn.88.1238186295892; Fri, 27 Mar 2009 13:38:15 -0700 (PDT) X-Mailman-Approved-At: Sat, 28 Mar 2009 09:33:50 +0100 X-BeenThere: petrinet@informatik.uni-hamburg.de X-Mailman-Version: 2.1.10 Precedence: list Original-Sender: petrinet-bounces@informatik.uni-hamburg.de Errors-To: petrinet-bounces@informatik.uni-hamburg.de Xref: news.gmane.org gmane.science.mathematics.petri-nets:1514 gmane.comp.mathematics.reliable-computing:1170 gmane.comp.science.concurrency:1549 gmane.science.mathematics.categories:203 Archived-At: --===============0965603931== Content-Type: multipart/alternative; boundary=0016364eed545523b604661fb6ec --0016364eed545523b604661fb6ec Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Call for Papers CFV'09: Sixth International Workshop on Constraints in Formal Verification Grenoble, France, June 25, 2009. A satellite event of the 21st International Conference on Computer Aided Verification (CAV'09) CFV'09 web site: http://www.miroslav-velev.com/cfv09.html Abstract submission deadline: April 15 Paper submission deadline: April 22 Overview --------------------------------------------- Formal verification is of crucial significance in the development of hardware and software systems. In the last few years, tremendous progress was made in both the speed and capacity of constraint technology. Most notably, SAT solvers have become orders of magnitude faster and capable of handling problems that are orders of magnitude bigger, thus enabling the formal verification of more complex computer systems. As a result, the formal verification of hardware and software has become a promising area for research and industrial applications. The main goals of the Constraints in Formal Verification workshop are to bring together researchers from the CSP/SAT and the formal verification communities, to describe new applications of constraint technology to formal verification, to disseminate new challenging problem instances, and to propose new dedicated algorithms for hard formal verification problems. This workshop will be of interest to researchers from both academia and industry, working on constraints or on formal verification and interested in the application of constraints to formal verification. Scope --------------------------------------------- The scope of the workshop includes topics related to the application of constraint technology to formal verification, namely: - application of constraint solvers to hardware verification; - application of constraint solvers to software verification; - dedicated solvers for formal verification problems; - challenging formal verification problems. Delivery --------------------------------------------- The workshop is scheduled for June 25, 2009. It will be structured to allow ample time for discussion and demonstration of new tools and new problem instances. Submissions --------------------------------------------- Submissions should be in the LNCS format and in one of the following types: - a regular paper of up to 15 pages; - a short paper of up to 4 pages, describing an industrial experience. Workshop papers should be submitted electronically in pdf format. Papers should be formatted using the Lecture Notes in Computer Science (LNCS) style. Paper submissions should be e-mailed to the workshop chairs at: mvelev@gmail.com Important Dates --------------------------------------------- The important dates for the workshop are as follows: - abstract submission deadline: April 15 - paper submission deadline: April 22 - notification of acceptance: May 10 - camera-ready version deadline: May 31 - workshop date: June 25 Invited Speakers --------------------------------------------- Bernd Becker, University of Freiburg, Germany Talk title: SAT and SMT Solving in a Multi-Core Environment Nikolaj Bjorner, Microsoft Research, U.S.A. Talk title: SMT Solving and Applications of Bit-Level Constraints Workshop Chair --------------------------------------------- Miroslav Velev, Aries Design Automation, U.S.A. Masahiro Fujita, University of Tokyo, Japan Program Committee -------------------------------------------- Jay Bhadra, Freescale, U.S.A. S=E9rgio Vale Aguiar Campos, Universidade Federal de Minas Gerais, Brazil Maciej Ciesielski, University of Massachusetts, U.S.A. Goerschwin Fey, University of Bremen, Germany Alex D. Groce, NASA-JPL, U.S.A. Michael Hsiao, Virginia Tech, U.S.A. Chung-Yang (Ric) Huang, National Taiwan University, Taiwan John Franco, University of Cincinnati, U.S.A. Priyank Kalla, University of Utah, U.S.A. Shin-ichi Minato, Hokkaido University, Japan Steve Prestwich, University College Cork, Ireland Andreas Veneris, University of Toronto, Canada --0016364eed545523b604661fb6ec Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable

Call for Papers

CFV'09:=A0 Sixth International Workshop on Constraints in Formal Verification

Grenoble, France, June 25, 2009.
A satellite event of the 21st Intern= ational Conference on
Computer Aided Verification (CAV'09)


CFV'09 web site: http://www.miroslav-velev.com/cfv09.html


Abstract submission deadline:=A0 April 15
Paper submission deadli= ne:=A0 April 22


Overview
---------------------------------------------
Formal = verification is of crucial significance in the development of
hardware a= nd software systems. In the last few years, tremendous
progress was made= in both the speed and capacity of constraint
technology. Most notably, SAT solvers have become orders of magnitude
fa= ster and capable of handling problems that are orders of magnitude
bigge= r, thus enabling the formal verification of more complex computer
system= s. As a result, the formal verification of hardware and software
has become a promising area for research and industrial applications.
Th= e main goals of the Constraints in Formal Verification workshop are
to b= ring together researchers from the CSP/SAT and the formal
verification c= ommunities, to describe new applications of constraint
technology to formal verification, to disseminate new challenging
proble= m instances, and to propose new dedicated algorithms for hard
formal ver= ification problems.
This workshop will be of interest to researchers fro= m both academia
and industry, working on constraints or on formal verification and
inter= ested in the application of constraints to formal verification.


Scope
---------------------------------------------
The scope = of the workshop includes topics related to the application
of constraint= technology to formal verification, namely:
- application of constraint = solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicate= d solvers for formal verification problems;
- challenging formal verific= ation problems.


Delivery
---------------------------------------------
The wor= kshop is scheduled for June 25, 2009. It will be
structured to allow amp= le time for discussion and demonstration of new
tools and new problem in= stances.


Submissions
---------------------------------------------
Subm= issions should be in the LNCS format and in one of the following types:
= - a regular paper of up to 15 pages;
- a short paper of up to 4 pages, d= escribing an industrial experience.
Workshop papers should be submitted electronically in pdf format.
Papers= should be formatted using the Lecture Notes in Computer Science
(LNCS) = style.
Paper submissions should be e-mailed to the workshop chairs at: <= br> mvelev@gmail.com<= /p>


Important Dates
---------------------------------------------
= The important dates for the workshop are as follows:
- abstract submissi= on deadline:=A0 April 15
- paper submission deadline:=A0 April 22
- n= otification of acceptance:=A0 May 10
- camera-ready version deadline:=A0 May 31
- workshop date:=A0 June 25


Invited Speakers
---------------------------------------------Bernd Becker, University of Freiburg, Germany
=A0 Talk title: SAT and S= MT Solving in a Multi-Core Environment

Nikolaj Bjorner,=20 Microsoft Research, U.S.A.
=A0=A0 Talk title: SMT Solving and Applications of Bit-Level Constraints

Workshop Chair
---------------------------------------------
Miros= lav Velev, Aries Design Automation, U.S.A.

Masahiro Fujita, University of Tokyo, Japan

=A0


Program Committee
--------------------------------------------Jay Bhadra, Freescale, U.S.A.

S=E9rgio Vale Aguiar Campos, Universidade Federal de Minas Gerais, Brazi= l

Maciej Ciesielski, University of Massachusetts, U.S.A.

Goerschwin Fey, University of Bremen, Germany

Alex D. Groce, NASA-JPL, U.S.A.

Michael Hsiao, Virginia Tech, U.S.A.

Chung-Yang (Ric) Huang, National Taiwan University, Taiwan

John Franco, University of Cincinnati, U.S.A.

Priyank Kalla, University of Utah, U.S.A.

Shin-ichi Minato, Hokkaido University, Japan

Steve Prestwich, University College Cork, Ireland

Andreas Veneris, University of Toronto, Canada

=A0

--0016364eed545523b604661fb6ec-- --===============0965603931== Content-Type: text/plain; charset="us-ascii" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Disposition: inline