Abstract
We propose the use of modern proof assistants to specify, implement, and verify password quality checkers. We use the proof assistant Coq, focusing on Linux PAM, a widely-used implementation of pluggable authentication modules for Linux. We show how password quality policies can be expressed in Coq and how to use Coq’s code extraction features to automatically encode these policies as PAM modules that can readily be used by any Linux system. We implemented the default password quality policy shared by two widely-used PAM modules: pam_cracklib and pam_pwquality. We then compared our implementation with the original modules by running them against a random sample of 100,000 leaked passwords obtained from a publicly available database. In doing this, we demonstrated a potentially serious bug in the original modules. The bug was reported to the maintainers of Linux PAM and is now fixed.

Abstract
Although there are several studies analysing how innovation capabilities influence export performance, this study aims to present the impact of a set of internal innovation capabilities on export performance of small and medium-sized firms (SMEs), with the mediating role of entrepreneurial orientation contingent upon the proactive or reactive behaviour of the firms to external stimuli. The study involves the analysis of 147 questionnaire-based survey of managers from plastic manufacturing SMEs operating in Portugal that were subjected to a Partial Least Squares-Structural Equation Modelling (PLS-SEM) technique. The results show that proactive firms to external stimuli are not only better at innovating but also their entrepreneurial orientation capabilities underpin a better performance in international markets when compared with firms that react to external stimuli. This study has implications for SMEs aiming at increasing their export performance and innovativeness. For practitioners the findings of this study should enable SMEs owner/managers to better understand the possible impacts of innovation capabilities and entrepreneurial orientation on export performance, and thus lead to more effective SMEs management.

Abstract
Exploring the seas and the oceans is essential for industrial and environmental applications. Given the fact that the seas cover 72% of the surface of the Earth and are home to 90% of all life found on it, underwater imaging has become an active research area in recent years. Due to the high absorption of electromagnetic waves by water, sonar is currently the exemplary choice used in underwater imaging. Yet, underwater images acquired with sonars suffer from various degradations, since the sound signal is affected by the environment and the sonar parameters and geometry. This work proposes an enhancement method that aims at getting close to natural underwater images. The enhanced images can be used in further applications related to seabed mapping and underwater computer vision. The enhancement aims at reducing the echo-decay and some effects of the receiver gain.

Abstract
The work described in this paper is part of the development of a framework to support the joint execution of cooperative missions by a group of vehicles, in a simulated, augmented, or real environment. Such a framework brings forward the need for formal languages in which to specify the vehicles that compose a team, the scenario in which they will operate, and the mission to be performed. This paper introduces the Scenario Description Language (SDL) and the Team Description Language (TDL), two Extensible Markup Language based dialects that compose the static components necessary for representing scenario and mission knowledge. SDL provides a specification of physical scenario and global operational constraints, while TDL defines the team of vehicles, as well as team-specific operational restrictions. The dialects were defined using Extensible Markup Language schemas, with all required information being integrated in the definitions. An interface was developed and incorporated into the framework, allowing for the creation and edition of SDL and TDL files. Once the information is specified, it can be used in the framework, thus facilitating environment and team specification and deployment. A survey answered by practitioners and researchers shows that the satisfaction with SDL+TDL is elevated (the overall evaluation of SDL+TDL achieved a score of 4 out of 5, with 81%/78.6% of the answers 4); in addition, the usability of the interface was evaluated, achieving a score of 86.7 in the System Usability Scale survey. These results imply that SDL+TDL is flexible enough to represent scenarios and teams, through a user-friendly interface.

Abstract
This paper presents an integrated cognitive robotics system for industrial kitting operations in a modern factory setting. The robot system combines low-level robot control and execution monitoring with automated mission and task planning, and a logistics planner which communicates with the factory's manufacturing execution system. The system has been implemented and tested on a series of automotive kitting problems, where collections of parts are picked from a warehouse and delivered to the production line. The system has been empirically evaluated and the complete framework shown to be successful at assembling kits in a small factory environment.

Abstract
This paper aims to develop grasping and manipulation capability along with autonomous navigation and localization in a wheelchair-mounted robotic arm to serve patients. Since the human daily environment is dynamically varied, it is not possible to enable the robot to know all the objects that would be grasped. We present an approach to enable the robot to detect, grasp and manipulate unknown objects. We propose an approach to construct the local reference frame that can estimate the object pose for detecting the grasp pose of an object. The main objective of this paper is to present the grasping and manipulation approach along with a navigating and localization method that can be performed in the human daily environment. A grid map and a match algorithm is used to enable the wheelchair to localize itself using a low-power computer. The experimental results show that the robot can manipulate multiple objects and can localize itself with great accuracy.