[TYPES] CFP: Workshop on Constraint Programming and Constraint for Verification (CP+CV'04)

[Giorgio Delzanno]

================================================================================ 


                           CALL FOR PAPERS


Workshop on Constraint Programming and Constraint for Verification 
(CP+CV'04)

                      March 28, Barcelona, Spain

 at the European Joint Conferences on Theory and Practice of Software 
(ETAPS)

            Home page: http://www.disi.unige.it/person/DelzannoG/CP+CV/

================================================================================ 


OVERVIEW

The use of constraints had its scientific and commercial breakthrough in
the 1990s.
Programming with constraints makes it possible to model and specify 
problems
with uncertain, incomplete information and to solve combinatorial problems,
as they are abundant in industry and commerce, such as scheduling, 
planning,
transportation, resource allocation, layout, design, and analysis.
Constraint-based programming languages enjoy elegant theoretical 
properties,
conceptual simplicity, and practical success.

The aim of the workshop is to provide opportunity for interactions with the
other ETAPS'04 events and to be a major meeting point in the research area
inbetween the Constraint Programming conferences, which are held each 
autumn.

The workshop will consist of sessions with invited talks that summarize the
main challenges and/or application potential for the community, and 
sessions
with short presentations describing ongoing work.

Taking inspiration from the CP 02 workshop CFV, we will have a special 
track
dedicated to "formal verification". In recent years there has been an
increasing  interest for the application of constraint programming and
constraint solving  technology to the formal verification of hardware
and software systems.
Constraint solvers for Boolean (SAT) and arithmetic domains (Presburger,
polyhedra,  linear constraints) are widely used as subprocedures of
symbolic model checkers  (e.g. nuSMV) and of model checkers for hybrid
and real time systems (e.g. HyTech, Uppaal).
Constraint solving is also used for computing static analysis of programs
with numerical data variables and concurrent systems (e.g. via the 
Structural
Theory of Petri Nets).

The aim of this special track is to bring together researchers working
in constraints  and verification and to investigate the theoretical
foundations, new applications,  and future developments in this area.

SUBMISSION

To submit, send an email to Giorgio Delzanno giorgio at disi.unige.it
containing four consecutive ASCII lines with title, author(s), email(s) and
WWW link directly to compressed  postscript file (5-15 pages).

Accepted papers will be available electronically at the workshop web-page
and may be published in hard-copy proceedings (available at the workshop).

ORGANISATION AND PROGRAM COMMITTEE

Giorgio Delzanno, DISI - University of Genova
Thom Fruehwirth, University of Ulm
Francois Fages, INRIA Rocquencourt
Joao Marques-Silva, Technical University of Lisbon, IST/INESC-ID/CEL
Andreas Podelski, MPI - Saarbruecken
Peter Stuckey, University of Melbourne

IMPORTANT DATES

January 28, 2004: Paper submissions
February 25, 2004: Acceptance decisions
March 12, 2004: Final version due
March 28, 2004: Workshop at ETAPS 2004