MVW 2016 - Meets Verification 2016 Workshop

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.
This 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. 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 an investigation on 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.
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 (see call for contributions),
space for questions and discussions.