Computing systems are getting ever more ubiquitous, making usdependent on their proper functioning. Therefore we require that theyare correct (i.e. they conform their intended behavior), safe (i.e.itsoperation does not have catastrophic consequences), reliable,available to provide the intended service, and secure (i.e., no userwithout appropriate clearance can access or modify protected data).Guarantees for such charcteristics rely on rigid specification andanalysis techniques for both the required system functionality as wellas its behavior. Formal methods provide a mathematical approach tomodel, understand, and analyze systems, especially at earlydevelopment stages.In this project we focus on three aspects of formal methods:specification, verification, and synthesis. We consider the study ofboth qualitative behavior and quantitative behavior (extended withprobabilistic information). We aim to study formal methods in alltheir aspects: foundations (their mathematical and logical basis),algorithmic advances (the conceptual basis for software toolsupport) and practical considerations (tool construction and casestudies).The MEALS project includes five tightly interconnected thematic workpackages. They focus on quantitative analysis of concurrent programbehaviour (WP1), reasoning tasks for specification and verification(WP2), security and information flow properties (WP3), synthesis inmodel-based systems engineering (WP4) and foundations for theelaboration and analysis of requirements specifications (WP5).The crosscutting concern of all these work packages is the development offormal techniques for the specification, verification and synthesis ofdependable ubiquitous computing systems. Five carefully planned MEALSgatherings and workshops give the project an effectve structure forknowledge transfer, communitiy building, and result dissemination,aimed at a sustained transcontinental collaboration.