Abstract. Ubiquitous computing, where computers 'disappear' and instead sensor-enabled and software-controlled devices assist us in every-day tasks, has become an established trend. To ensure the safety and reliability of software embedded in these devices, rigorous model-based design methodologies are called for. Quantitative verification, a powerful technique for analysing system models against quantitative properties such as "the probability of a data packet being delivered within 1ms to a nearby Bluetooth device is at least 0.98", has proved useful by detecting and correcting flaws in a number of ubiquitous computing applications. In this paper, we focus on three key aspects of ubiquitous computing: autonomous behaviour, constrained resources and adaptiveness. We summarise recent advances of quantitative verification in relation to these aspects, illustrating each with a case study analysed using the probabilistic model checker PRISM. The paper concludes with an outline of future challenges that remain in this area.