ABSTRACT. Autonomous systems are key to the IoT vision promising increasing integration of smart services and systems minimizing human intervention. This vision challenges our capability to build next-generation autonomous systems that (i) exhibit “broad intelligence” being able to manage a dynamically changing set of potentially conflicting goals; (ii) interact with complex and unpredictable environments involving cyber physical components; (iii) can harmoniously collaborate with human operators.

We advocate that there is a strong and urgent need to lay out a common engineering foundation for the development of next-generation autonomous systems. Among the open issues that the foundation should address are (i) robust design methodologies integrating model-based and data-based techniques; (ii) means for faithful modeling and simulation of a system in its physical environment (which includes humans); (iii) the combination of empirical and proof-based validation techniques for assessing trustworthiness and performance.

We conclude arguing that building trustworthy next-generation autonomous systems goes for far beyond the current AI challenge.

ABSTRACT. Random testing works very well in practice, but often we do not know why. In this tutorial, we shall explore techniques from randomized algorithms and combinatorics that enable us to provide theoretical results about the performance of random testing procedures in different situations. On the one hand, these techniques provide insight into the workings and effectiveness of the testing procedures. On the other, they help us build new algorithms.

ABSTRACT. This tutorial describes the most important ideas of SAT solvers based on conflict driven clause learning, which is the dominant solver paradigm in SAT applications. Basics techniques include clause learning, the notion of implication graph, as well as clause minimization. We further discuss restarts and garbage collecting useless learned clauses. Efficient data structures for boolean constraint propagation are essential too.

ABSTRACT. We present some basics of game theory, focusing on matrix games. We then present the model of multiplayer stochastic concurrent games (with an underlying graph), which extends standard finite-state models used in verification in a multiplayer and concurrent setting; we explain why the basic theory cannot apply to that general model. We then focus on a very simple setting, and explain and give intuitions for the computation of Nash equilibria. We then give a number of undecidability results, giving limits to the approach. Finally we describe the suspect game construction, which (we believe) captures and explains well Nash equilibria and allow to compute them in many cases.