The 20th International Conference on
Principles and Practice of
Constraint Programming
Lyon, France
8-12 September 2014

CP meets Verification 2014

Theme

This workshop (on Monday 8 September 2014) gathers researchers and practitioners from constraint programming (CP), formal verification, and software engineering, in order to address the CP-based solving of challenging constraint problems in formal verification and software engineering. Solvers of CP technology are orthogonal but complementary to solvers of technologies like SAT, SAT modulo theories (SMT), integer programming (IP), and mixed integer programming (MIP).

Objectives

The objectives of this workshop are:

  • The delegates with a non-CP background present challenging constraint problems in formal verification and software engineering, as well as current solution approaches (whether ad hoc or based on SAT, SMT, IP, or MIP technology), towards investigation using a (hybrid with a) CP solver.
  • The delegates with a CP background present either CP solvers or how they have successfully used CP technology for challenging constraint problems in formal verification and software engineering.
  • All delegates, whether presenters or not, discuss synergy opportunities as well as challenges in formal verification, software engineering, and the underlying constraint solving tools.

The first edition of this workshop was a one-week seminar in 2012: see CP meets Verification 2012.

Programme

See the map for locations:

09:00 - 09:05 Opening, in room 337 of building "Blaise Pascal"
09:05 - 10:00 Invited Talk 1: Some Uses of Constraints in Program Analysis and Verification (Slides)
Andreas Podelski, University of Freiburg, Germany
10:00 - 10:30 Tea, in building "La Rotonde"
10:30 - 11:00 CP meets SMT (Abstract) (Slides)
François Bobot, Sébastien Bardin, and Bruno Marre
11:00 - 11:30 Towards an Effective Formally Certified Constraint Solver (Abstract) (Slides)
Catherine Dubois and Arnaud Gotlieb
11:30 - 12:00 Interactive Configuration Verification using CP (Abstract) (Slides)
Razieh Behjati and Shiva Nejati
12:00 - 12:30 Solving the Address Translation Problem as a CSP (Abstract) (Slides)
Eyal Bin and Elad Venezian
12:30 - 14:00 Lunch (included), in restaurant "Au pied du saule"
14:00 - 14:30 Avoiding Saturation in Sound Processes with CP (Abstract) (Slides)
Charlotte Truchet, Julie Laniau, and Yann Orlarey
14:00 - 15:00 A Constraint-Solving Approach to Faust Program Type Checking (Abstract) (Slides)
Imré Frotier de la Messelière, Pierre Jouvelot, and Jean-Pierre Talpin
15:00 - 16:00 Invited Talk 2: Verification by Second-Order Constraint Solving: Applications, Methods, Challenges (Abstract) (Slides)
Philipp Rümmer, Uppsala University, Sweden
16:00 - 16:30 Tea, in building "La Rotonde"
16:30 - 17:00 On CP Capabilities for Verifying Programs With Floating-Point Computation (Abstract) (Slides)
Michel Rueher, Hélène Collavizza, Claude Michel, Olivier Ponsini, and Mohammed Said Belaid
17:00 - 17:30 Query-Based Symbolic Execution (Abstract) (Slides)
Kathryn Francis and Peter J. Stuckey
17:30 - 18:00 Protocol Log Analysis with CP (Abstract) (Slides)
Kenneth Balck, Mats Carlsson, Olga Grinchtein, and Justin Pearson
18:00 - 18:30 Bounded Strings for Constraint Programming (Abstract) (Slides)
Joseph D. Scott, Pierre Flener, and Justin Pearson

Sponsorship

This workshop is sponsored by the Certus Centre for Software Verification & Validation at the SIMULA Research Laboratory, Norway.

Certus-SFI

Form

This is a call for abstracts, not a call for papers. Abstracts of at most one page, in text or PDF form, are to be emailed by the deadline below. If anything is unclear about this call, then contact the main organiser. The talks most compliant with the workshop theme and objectives above will be selected for presentation in a full-day workshop. There will be no papers and no proceedings, but the slides of the presentations will be archived on this website.

All researchers and practitioners within the scope of the workshop are invited to attend, whether as presenters or not, so as to stimulate good discussions.

Depending on the success of the workshop, a special issue at a journal will be arranged (details to be announced).

The participation cost is the workshop fee of the CP 2014 conference.

Important Dates

  • Wednesday 25 June 2014: Early abstract submission deadline, by email to cpcav14@gmail.com, with notification minimum 7 days before the early registration deadline of CP 2014 (on 9 July)
  • Monday 4 August 2014: Late abstract submission deadline, by email to cpcav14@gmail.com, with notification on 11 August 2014
  • Monday 8 September 2014: Workshop (all day), in Lyon, France

Organisers