Home > Projects > FREETECH

FreeTech

Formal Reasoning for Enabling and Emerging Technologies

Basic data

Field

National

Date

01/01/2019 - 31/12/2021

Industry

Otros
Salud

Budget

242000

Funded by

State Investigation Agency

Website

Video

PROJECT INFORMATION

DESCRIPTION

The use of techniques based on formal reasoning has been successfully used to ensure the reliability, efficiency and safety of technological products. The focus of the FREETech project is the following: (1) the development of program analysis, verification, testing and debugging techniques that allow reasoning about correctness, efficiency and possible vulnerabilities in both existing and emerging applications. These applications include software-defined networks or smart contracts for which resource consumption and security are highly relevant, as well as communication protocols with physical properties such as real time or distances; (2) the use of data science and machine learning techniques to obtain, develop and/or manipulate models of current applications; (3) the use of formal reasoning to improve search techniques in genomic sequences; or (4) the use of constraint solving and optimization tools and techniques (SAT, SMT and CP) to address complex planning and replanning problems.
In this way, our project covers from the basic theory for the development and application of existing enabling technologies to the current challenges introduced by emerging information technologies in the digital society.

Impact

The techniques and tools that are based on formal reasoning are having a great impact on many areas of application of Information Technology, as well as in the search for solutions to the different computational problems that turn out in digital economy and society, and security and defense, but also the ones that arise in health, energy efficiency or smart and sustainable transport challenges.
The leading technology companies, such as Facebook, Amazon and Google, are banking on the use of formal reasoning for the development and implementation of their technology. Recently, in the Federation of Conferences FLOC (Federated Logic Conference 2018), a
workshop on Formal Methods in Industry was held (https://www.floc2018.org/formal-methods-in-industry), where the leader researchers from the three above-mentioned companies explained how the formal reasoning has become the cornerstone of their technological development processes. Byron Cook, professor at University College of London and director of the Automated Reasoning Group (ARG) at Amazon Web Services (AWS) related, as an example of the enormous impact that these techniques can have in his sector, that AWS uses and develops tools based on formal reasoning to detect and avoid security problems both in AWS and in the systems that are created by the customers over AWS.
As another example of direct impact, the optimization techniques based on logic and formal reasoning may report an important benefit in the enterprise environment. The flexibility that characterizes these methods offers to the organizations a quick technology which is able to improve their results in a variety of scenarios.
Formal reasoning achieves even more importance in the most emerging areas of application, such as smart-contracts used in blockchain technologies, software-defined networks, bioinformatics, communication protocols or the more frequent use of learning techniques in a multitude of environments and applications. The techniques based on formal reasoning are essential to reach the objectives of the project, which result in applications with a major economic and social impact as blockchain technology, software-defined networks, industrial planning and programming or resources located in the cloud, program analysis, security, the discovery of knowledge and web data manipulation or the detection of some genome sequences.
As the scientific histories of the different research groups involved in the proposal guarantee, the expected scientific international impact of the objectives and results that the project pursues is expected to be large and it is expected to publish them in conferences and journals internationally recognized and with high impact. To conclude, it is expected that project FREETech reaches a significant national and international impact, both on the advance of science and technology and its transfer to public and private companies and organizations.