In Norway, cervical cancer prevention involves the participation of as many eligible women aged 25-69 years as possible. However, reaching and inviting every eligible women to attend cervical cancer screening and HPV vaccination is difficult. Using social nudging and gamification in modern means of communication can encourage the participation of unscreened people. Simula Research Laboratory together with the Cancer Registry of Norway have developed FightHPV, a mobile app game intended to inform adolescent and eligible women about cervical cancer screening and HPV vaccination while they play and, to facilitate their further participation to prevention campaigns. However, game design and health information transfer can be hard to reconcile, as the design of each game episode is more guided by the release of information than gameplay and playing difficulty. In this paper, we propose a constraint-based model of FightHPV to evaluate the difficulty of each episode and to help the game designer in improving the player experience. This approach is relevant to facilitate social nudging of eligible women to participate to cervical cancer screening and HPV vaccination, as shown by the initial deployment of FightHPV and tests performed in focus groups. The design of this mobile app can thus be regarded as a new application case of Artificial Intelligence techniques such as gamification and constraint programming.

We present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names).