Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference - the latter being a variant of Nelson's biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non -monotonic program combinators.

Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.

Abstract
Approximate agreement has long been relegated to the sidelines compared to exact consensus, with its most notable application being clock synchronisation. Other proposed applications stemming from control theory target multi-agent consensus, namely for sensor stabilisation, coordination in robotics, and trust estimation. Several proposals for approximate agreement follow the Mean Subsequence Reduce approach, simply applying different functions at each phase. However, taking clock synchronisation as an example, applications do not fit neatly into the MSR model: Instead they require adapting the algorithms' internals. Our contribution is two-fold. First, we identify additional configuration points, establishing a more general template of MSR approximate agreement algorithms. We then show how this allows us to implement not only generic algorithms but also those tailored for specific purposes (clock synchronisation). Second, we propose a toolkit for making approximate agreement practical, providing classical implementations as well as allow these to be configured for specific purposes. We validate the implementation with classical algorithms and clock synchronisation.

Abstract
The development of more flexible and robust models for reasoning about systems in environments with potentially conflicting information is becoming more and more relevant in different contexts. In this direction, we recently introduced paraconsistent transition systems, i.e. transition systems whose transitions are tagged with a pair of weights, one standing for the degree of evidence that the transition exists, another weighting its potential non existence. Moreover, these structures were endowed with a modal logic [3] that was further formalised as an institution in [5]. This paper goes a step further, proposing an approach for the structured specification of paraconsistent transition processes, i.e. paraconsistent transition systems with initial states. The proposed approach is developed along the lines of [12], which introduced a complete methodology for (standard) reactive systems development building on the Sannella and Tarlecki stepwise implementation process. For this, we enrich the logic with dynamic modalities and hybrid features, and provide a pallet of constructors and abstractors to support the development process of paraconsistent processes along the entire design cycle.

Abstract
Immersive video applications impose unpractical bandwidth requirements for best-effort networks. With Multi-View(MV) streaming, these can be minimized by resorting to view prediction techniques. SmoothMV is a multi-view system that uses a non-intrusive head tracking mechanism to detect the viewer's interest and select appropriate views. By coupling Neural Networks (NNs) to anticipate the viewer's interest, a reduction of view-switching latency is likely to be obtained. The objective of this paper is twofold: 1) Present a solution for acquisition of gaze data from users when viewing MV content; 2) Describe a dataset, collected with a large-scale testbed, capable of being used to train NNs to predict the user's viewing interest. Tracking data from head movements was obtained from 45 participants using an Intel Realsense F200 camera, with 7 video playlists, each being viewed a minimum of 17 times. This dataset is publicly available to the research community and constitutes an important contribution to reducing the current scarcity of such data. Tools to obtain saliency/heat maps and generate complementary plots are also provided as an open-source software package.

Abstract
There are several educational software (ES) used in the classroom environment for the teaching and learning of geometric contents that are part of the Portuguese basic education mathematics program. There are studies that show that the use of this type of artifact has a fundamental role in the behavior of students, raising, among other aspects, a greater motivation for learning mathematics. The aim of this work is to explore and describe implications for the behavior and learning of students in the 7th grade of Portuguese basic education, in face of a pedagogical practice that involves carrying out tasks using ES Plickers, in the theme similarities of the domain geometry and measurement, throughout intervention carried out. The adopted methodology presents characteristics of a quasi-experimental study. The participants were 61 students from three classes of a school in the north of Portugal, followed during eight consecutive classes. A set of tasks using Plickers, tests and a questionnaire survey were used as instruments for data collection. The results point to positive increments, at a behavioral level, as well as in the evolution of learning, in view of the use of this methodology in the classroom.