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

March 28, 2004, Barcelona, Spain

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

Important: Early registration ** February 15 **

Detailed registration information are available at the ETAPS on-line registration page.
It is possible to register for the workshop without registering for the main conference.

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, andpractical 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.

Preliminary Program

Session I: Data structures and applications of constraint-based verification

09.15 - 10.00: Invited talk

    Ahmed Bouajjani - University of Paris 7
   Constraints for the Verification of Infinite-state Systems

10.00 - 10.30: coffee 

10.30 - 11.15: Invited talk

   Bernard Boigelot - University of Liege
   Automata-based Representations of Arithmetic Constraints
   Abstract   Slides pdf


11.15 - 12.00: Invited talk

  Wang Yi -  Uppsala University   
  Difference Clock Constraints and Termination in UPPAAL: "the so-called bug"

12.00 - 12.30: Technical contribution

  Pierre Ganty and Laurent Van Begin - University of Bruxelles   
  Non deterministic Automata for the Efficient Verification of Infinite-state Systems
  Abstract (ps)    Slides (pdf)

12.30 - 14.00: LUNCH

Session II: Constraint-based software verification

14.00 - 14.45: Invited talk

 
Markus Mueller-Olm, University of Dortmund
  Precise Program Analysis with (Linear) Algebra
  Abstract    Slides (pdf)


14.45 - 15.30: Invited talk

  Cormac Flanagan - University of California at Santa Cruz
  Software Model Checking and Constraint Programming
  Paper (ps)     Slides (pdf)

15:30-16.00: coffee break

16.00 - 16.30: Technical contribution

  Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, and Konrad Slim - University of Utah

  A Unified Framework for Handling Constraints During Program Analysis
  Abstract (pdf)     Slides pdf

Session III: Non-standard applications and theorem proving

16.30 - 17.00: Invited talk

  Francois Fages - INRIA Roquencort
  Constraint-based Model Checking of  Non-deterministic Hybrid Systems:
  A First Experiment in Systems Biology
  Slides ppt

17.00 - 17.30: Technical contribution

  Marco Cadoli and Toni Mancini - University of Rome "La Sapienza"
  Using a Theorem Prover for Reasoning on Constraint Problems
  Paper (ps)    Slides (pdf)

17.30-18.00: Discussion

Important Dates

January 28, 2004: Paper submissions
February 15, 2004: Early registration date
February 25, 2004: Final version due
March 28 , 2004: Workshop at ETAPS 2004

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 Max Planck Institut fuer Informatik - Saarbruecken
Peter Stuckey University of Melbourne