postings]
Third Workshop « CP meets Verification 2016 »
Co-located event of CP 2016 (http://cp2016.a4cp.org/)
Toulouse, France – September 5th 2016
Website: http://cp2016.a4cp.org/program/workshops/ws-cpcav16.html
== IMPORTANT DATES ==
Submission: June 4, 2016 (*deadline extension*)
Notification: July 15, 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@cea.fr
== Workshop Chairs ==
– Sébastien Bardin (CEA LIST, France)
– François Bobot (CEA LIST, France)
– Nikolai Kosmatov (CEA LIST, France)
Contact: cpmeetsverif16@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
—
Nikolai KOSMATOV, PhD
Software Safety Laboratory, CEA LIST
Mail : CEA Saclay Nano-INNOV
Institut CARNOT CEA LIST
DILS/LSL, PC 174
91191 Gif-sur-Yvette Cedex, France
Phone: +33 (0)1 69 08 71 83
Fax: +33 (0)1 69 08 83 95
Email: nikolai.kosmatov@cea.fr