Overview

In the everlasting quest for safer and more reliable systems, academic research and industrial interest have taken many avenues. The most populous of these avenues are testing, formal verification, and analysis, and on such avenues there is a particular family of approaches that proved remarkably efficient: the constraint-based family.

For decades, the constantly evolving communities of constraint programming (CP), Boolean satisfiability (SAT), and -more recently- satisfiability modulo theories (SMT) strived to explore to their fullest the capabilities of their respective technologies in key aspects such as expressivity, efficiency, scaling and handling of more theories. They often achieved great leaps through cross-fertilization between one another (conflict-driven learning, backjumping, variable selection heuristics,...). Indeed, even in the earliest editions of the CP conference, for example, one can find publications showing that bridging the gaps between these technologies can prove fruitful to each of them.

Their increasing efficiency further widened their attractiveness to domains such as software engineering, where existing applications such as symbolic execution methods were able to scale to previously unattained heights. Furthermore, unexpected applications for the constraint-family of technologies were uncovered, for example in software product lines, equivalence checking, security, automated exploit construction and fault localization methods.

The CSTVA workshop merged with the CP meets Verif workshop, under the name of CSTVA. This workshop aims at harnessing the potential of cross-fertilizations between CP, SAT and SMT to to contribute to verification, testing and analysis, preserving and increasing this momentum by bringing together all the aforementioned constraint communities as well as software/hardware verification, testing, analysis and engineering researchers and practitioners. Such a reunion has the potential for raising awareness about the capabilities of constraint solving and constraint optimization, encouraging the development of new applications based on tunable, extensible, programmable solvers, and uncovering new advances of any of the constraint-based technologies as well as their hybridization and cross-fertilization.

The CSTVA workshop therefore traditionally welcomes contributions of :
  • delegates with a constraint solving and optimization background (CP, SMT and SAT) presenting either new solvers or successful use of constraint-based technology to address constraint problems in formal verification and software engineering,
  • delegates with background in formal verification and software engineering, presenting challenging or unsolved problems, or insufficiencies to current solutions to those problems, prompting constraint-based investigations,
  • all delegates discussing 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, and following the success of the format adopted at the last CP meets Verif edition, the workshop is usually organized around:
  • several invited talks (at least half of the talks) given by experts of the different domains,
  • accepted talks based on a lightweight reviewing of submitted abstracts and papers, presenting either original or published works (see call for contributions),
  • space for questions and exchange, possibly through panel discussions.

There are no proceedings for the workshop, but slides and abstract / papers will be made available online.