[SMT-LIB] CFP: workshop CP meets verification (September 5, 2016, Toulouse, France)

[François Bobot]

==  CALL FOR ABSTRACTS ==

Third Workshop "CP meets Verification 2016"

Co-located event of CP 2016 (http://cp2016.a4cp.org/)
Toulouse, France - September 5th 2016

Web site: http://cp2016.a4cp.org/program/workshops/ws-cpcav16.html

== IMPORTANT DATES ==

Submission:   	June 27, 2016
Notification: 	July 8, 2016
Workshop: 	September 5, 2016


== THEMES AND OBJECTIVES ==

*Constraint programming* (CP) is a programming paradigm for the modelling and solving of constrained 
problems, such as complex problems in resource allocation, scheduling, configuration, and design. 
The success of CP comes from the fact that it provides high-level languages for declaratively 
modelling a problem by means of constraints that capture combinatorial substructures (and by means 
of an objective function) and for writing an efficient search procedure that solves the problem. 
*Computer-aided program verification* has found widespread applications in both academia and 
industry in ensuring that systems are dependable and secure. The discipline is based on fundamental 
mathematical theories such as logic and automata, and covers algorithmic techniques for formal 
analysis and synthesis, such as model checking, satisfiability (SAT) solving, and satisfiability 
modulo theories (SMT). These techniques have become essential tools for the design and analysis of 
hardware and software systems.

The "CP meets Verification" workshop 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* and 
foster novel ideas between CP and formal verification, since 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).

As the workshop aims at fostering lively discussions and debates between participants, it will be 
organized around
- several invited talks given by experts of the corresponding domains,
- accepted talks based on a lightweight reviewing of submitted abstracts,
- space for questions and discussions.

The CP meets Verification 2016 workshop invites all interested participants to *submit an abstract* 
of a talk to be presented during the workshop. Talks may present both original or already published 
work, tool developments as well as work in progress. Talks with emphasis on novel ideas or 
challenges are particularly welcome! Abstracts of at most one page, in text or PDF form, should be 
submitted by Email by the deadline given below. The talks most compliant with the workshop theme and 
objectives will be selected for presentation in a full-day workshop. For all inquiries, please 
contact the organizers.

The workshop will not require paper submission and will not publish proceedings, but the presenters 
will be invited to submit the slides of their talks for publication on the workshop website.

All researchers and practitioners interested in the scope of the workshop, whether presenters or 
not, are invited to attend the workshop and to participate in discussions.

Inquiries and submission of abstracts by Email: cpmeetsverif16 at cea.fr


== Workshop Chairs ==

- Sébastien Bardin (CEA LIST, France)
- François Bobot (CEA LIST, France)
- Nikolai Kosmatov (CEA LIST, France)

Contact: cpmeetsverif16 at cea.fr


== List of topics (not limited to) ==

- CP-based verification
- CP-based software engineering
- challenges in formal verification where CP can be helpful
- synergies between CP and verification technologies (model checking, abstract interpretation, etc.)
- synergies between CP, SAT, SMT, IP and/or MIP