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).
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.
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
This workshop is sponsored by the Certus Centre for Software Verification & Validation at the SIMULA Research Laboratory, Norway.
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.
Wednesday 25 June 2014: Early abstract submission deadline, by email to firstname.lastname@example.org, 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 email@example.com, with notification on 11 August 2014
- Monday 8 September 2014: Workshop (all day), in Lyon, France