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
Computer-aided program verification (CAV) 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.
CP meets CAV
The objective of this invitational seminar was for the CP and CAV communities to identify synergetic opportunities as well as challenges for the two communities in program verification and the underlying tools.