Refinement types are a type-based, static verification technique designed to be practical. They enrich the types of an existing programming language with logical predicates to specify program properties and automatically validate these specifications using SMT solvers. Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security. The weakness of refinement types is that they do not meet the soundness standards set by theorem provers. A sound verification system accepts as safe only those programs that never violate their specifications. Refinement type checkers (e.g., Liquid Haskell, F*, and Stainless) approximately report five unsoundness bugs per year, as opposed to only one reported by the Coq theorem prover. This rarity of unsoundness bugs in Coq is unsurprising since Coq is designed to soundly machine check mathematical proofs. Coq's soundness design recipe though cannot be directly applied to refinement type checkers that aim to practically verify real world programs. The goal of CRETE is to design a sound and practical refinement type system. This is an ambitious goal that entails the development of a verification system that is as practical as refinement types and constructs machine-checked mathematical proofs. The system will be implemented on refinement type systems for mainstream languages (i.e., Haskell and Rust) and will be evaluated on real-world code, such as web applications and cryptographic protocols. CRETE is high-risk since it aims to develop a novel program logic in which SMT automation co-exists with real world programming. Yet, CRETE is high-gain since it proposes a low-cost, high-profit approach to formal verification that aims to be integrated in mainstream software development.

The objective of the NEXTLEAP project is to build the fundamental interdisciplinary internet science necessary to create decentralized, secure, and rights-preserving protocols for the next generation of collective awareness platforms. The long-term goal of NEXTLEAP is to have Europe take the “next leap ahead” of the rest of the world by solving the fundamental challenge of determining how both to scientifically build and how to help citizens and institutions adopt open-source decentralized and privacy-preserving digital social platforms in contrast to proprietary centralized cloud-based services and pervasive surveillance that function at the expense of rights and technological sovereignty.

Distributed ledgers (DLs), also called blockchains, have the potential of transforming the ways individuals and businesses interact. While today a trusted third party, such as a bank, is required to guarantee that transactions among these entities are performed correctly, with DLs it is possible to delegate this task to a distributed computer network that relies on cryptographic operations and sophisticated distributed consensus algorithms to ensure that transactions are recorded durably and in a tamper-free manner. As a result, DLs have the potential to reduce the cost of transactions and the associated latencies dramatically. However, the adoption of DLs outside of crypto-currency use-cases has been slow partially due to their low performance compared to traditional data management systems. This stems mostly from the constraints and design choices inherited from the first public blockchains, that targeted public, geo-distributed, operation. Today, however, most industry use-cases require permissioned access to the ledger and involve nodes that are geographically close to each other (e.g. in a shipping port). This prompts a redesign of DLs and allows for using various hardware acceleration features to increase their performance. In the ACCORD project, we aim to increase distributed ledger throughput by at least an order of magnitude, while lowering latencies by a similar factor. To achieve this, we focus on the core component of DL systems, namely, distributed consensus that is used to establish an absolute order of transactions. This ordering operation (service) is typically the main performance bottleneck in DLs. To fully exploit emerging network technologies and to overcome stagnating CPU performance, we will use hardware acceleration (i.e., FPGAs) to offload the steps required by the ordering service. The outcome of this project is a DL design with performance that allows it to be deployed in use-cases in which DLs are inadequate today (e.g., trading).

The demand for larger and more interconnected software systems is constantly increasing, but the ability of developers to satisfy it is not evolving accordingly. The most limiting factor is software validation, which typically requires very costly and complex testing processes. This project aims at significantly improving the efficiency and effectiveness of the testing process and, with it, the overall quality of large software systems. For this, we propose to apply the “divide-and-conquer” principle, which is commonly used for architecting complex software, to testing by developing a novel test orchestration theory and toolbox enabling the creation of complex test suites as the composition of simple testing units. This test orchestration mechanism is complemented with a number of tools that include: (1) Capabilities for the instrumentation of the Software under Test enabling to reproduce real-world operational conditions thanks to features such as Packet Loss as a Service, Network Latency as a Service, Failure as a Service, etc. (2) Reusable testing services solving common testing problems including Browser Automation as a Service, Sensor Emulator as a Service, Monitoring as a Service, Security Check as a Service, Log Ingestion and Analysis as a Service, Cost Modeling as a Service, etc. (3) Cognitive computing and machine learning mechanisms suitable for ingesting large amounts of knowledge (e.g. specifications, logs, software engineering documents, etc.) and capable of using it for generating testing recommendations and answering natural language questions about the testing process. The ElasTest platform thus created shall be released basing on a flexible Free Open Source Software and a community of users, stakeholders and contributors shall be grown around it with the objective of transforming ElasTest into a worldwide reference in the area of large software systems testing and of guaranteeing the long term sustainability of the project generated results.