Today the cloud market is restricted to few providers, which entails higher prices, vendor lock-in and lower service quality. Smart Contracts (SC) and blockchain could reshape this market since they lower costs and provide trust without resorting to intermediaries. This paradigm, named blockchain-based clouds, prevents vendor lock-in and has the potential to make market's barriers so low that anyone with idle or spare computational resources can offer cloud services. The STARCloud project systematically utilises formal methods for the static analysis and runtime control of the next generation clouds for creating support for Quality of Service (QoS). To this aim, since the state-of-the-art solutions cannot be used in this domain, this project provides novel approaches and tools, including consensus mechanisms, a domain specific language for QoS definitions and QoS formal analysis tools, and a framework for the matchmaking and negotiation of SCs. Supporting QoS will boost the adoption of decentralised clouds; thus reducing prices and environmental impact; and improving QoS, which make the cloud providers and consumers that use blockchain-based clouds more competitive, specially in Europe, where the most advanced commercial solutions are located. Moreover, these solutions will enable geographically sparse micro and traditional cloud providers to join the market, which will leverage cloud and edge computing in Europe. The project is timely and, besides involving collaborators from many of the best European research institutes, it is supervised by I. Brandic, one of the main cloud experts in the world and actively involves one of the main players in the market: iExec. Overall, the solutions proposed here will contribute to the disruptive blockchain-based cloud paradigm and find immediate use in industry and academia by addressing the fundamental requirement of most cloud consumers, in particular business: QoS definition and enforcement in completely distributed systems.

“Entropy engineering” recently had exceptional impact on bulk materials science by invention of bul“Entropy engineering” recently had exceptional impact on bulk materials science by invention of bulk high entropy alloys and ceramics. The underlying idea is that by equiatomically adding ≥5 principal elements to alloys/compounds, the much increased configurational entropy stabilizes otherwise non-accessible single “high entropy” phases with an unique random elemental occupancy on a crystalline lattice and hence novel functional properties. Likewise, reducing dimensionality in “two-dimensional” (2D) materials recently had exceptional impact on materials science due to the 2D materials’ unique functional properties. Despite these exciting individual prospects of “entropy engineering” and “2D materials”, combination of these two concepts to synergetically create novel 2D high entropy materials (2D HEMs) as a novel materials class with novel functional properties with possible applications in electronics and catalysis remains lacking. In “HighEntropy2d” we will fabricate unprecedented 2D HEMs (2D high entropy alloys, oxides and sulfides) using for the first time scalable vapour deposition and a 2D template/2D confinement approach for both 2D film and 2D nanoflake form, asses their novel properties and perform first tests of their applicability for electronic devices and catalysis. Reducing HEM dimensionality to 2D will also create a unique opportunity to for the first time study in situ and at the atomic scale currently unknown fundamental diffusion, crystallisation, phase transition and separation mechanisms in HEMs (using a globally unique (scanning) transmission electron microscopy ((S)TEM) setup), to obtain fundamental insights relevant to HEMs even beyond the here newly introduced 2D HEMs. The proven track record of principal applicant Bernhard C. Bayer in 2D materials synthesis and atomic scale in situ (S)TEM is an ideal basis for this ambitious research programme.

The long list of software failures over the past years calls for serious concerns in our digital society, creating bad reputation and adding huge economic burden on organizations, industries and governments. Improving software reliability is no more enough, ensuring software reliability is mandatory. Our project complements other advances in the area and addresses this demand by turning first-order theorem proving into an alternative, yet powerful approach to ensuring software reliability, Saturation-based proof search is the leading technology for automated first-order theorem proving. The high-gain/high-risk aspect of our project comes from the development and use of saturation-based theorem proving as a unifying framework to reason about software technologies. We use first-order theorem proving methods not only to prove, but also to generate software properties that imply the absence of program errors at intermediate program steps. Generating and proving program properties call for new methods supporting reasoning with both theories and quantifiers. Our project extends saturation-based first-order theorem provers with domain-specific inference rules to keep reasoning efficient. This includes commonly used theories in software development, such as the theories of integers, arrays and inductively defined data types, and automation of induction within saturation-based theorem proving, contributing to the ultimate goal of generating and proving inductive software properties, such as invariants. Thanks to the full automation of our project, our results can be integrated and used in other frameworks, to allow end-users and developers of software technologies to gain from theorem proving without the need of becoming experts of it.